diff --git a/ulib/FStar.ReflexiveTransitiveClosure.fst b/ulib/FStar.ReflexiveTransitiveClosure.fst index 03cb02a99e7..c6e2a6097ad 100644 --- a/ulib/FStar.ReflexiveTransitiveClosure.fst +++ b/ulib/FStar.ReflexiveTransitiveClosure.fst @@ -27,6 +27,20 @@ type _closure (#a:Type u#a) (r:binrel u#a u#r a) : a -> a -> Type u#(max a r) = let _closure0 (#a:Type) (r:binrel a) (x y: a) : prop = squash (_closure r x y) +let rec induct_ (#a:Type) (r:binrel a) (p: a -> a -> prop) + (f_refl: (x:a -> squash (p x x))) + (f_step: (x:a -> y:a { r x y } -> squash (p x y))) + (f_closure: (x:a -> y:a -> z:a { p x y /\ p y z } -> squash (p x z))) + (x:a) (y:a) (xy:_closure r x y) +: Tot (squash (p x y)) (decreases xy) += match xy with + | Refl x -> f_refl x + | Step x y _ -> f_step x y + | Closure x y z xy yz -> + let p1 = induct_ r p f_refl f_step f_closure x y xy in + let p2 = induct_ r p f_refl f_step f_closure y z yz in + f_closure x y z + let get_squash (#a:Type) (r:binrel a) (x:a) (y:a{_closure0 r x y}) : Tot (squash (_closure r x y)) = assert_norm (_closure0 r x y ==> squash (_closure r x y)) @@ -159,3 +173,13 @@ let stable_on_closure #a r p hr = let xy = intro () in let xy : _closure r x y = unquote (binding_to_term xy) in exact (quote (_stable_on_closure r p hr x y xy (Squash.get_proof _)))) + +let induct + (#a:Type) (r:binrel a) (p: a -> a -> prop) + (f_refl: (x:a -> squash (p x x))) + (f_step: (x:a -> y:a { r x y } -> squash (p x y))) + (f_closure: (x:a -> y:a -> z:a { p x y /\ p y z } -> squash (p x z))) + (x:a) (y:a) (xy:squash (closure r x y)) +: squash (p x y) += let xy = FStar.Squash.join_squash #(_closure r x y) xy in + FStar.Squash.bind_squash xy (induct_ r p f_refl f_step f_closure x y) diff --git a/ulib/FStar.ReflexiveTransitiveClosure.fsti b/ulib/FStar.ReflexiveTransitiveClosure.fsti index c86f0251bd7..a5ca566e010 100644 --- a/ulib/FStar.ReflexiveTransitiveClosure.fsti +++ b/ulib/FStar.ReflexiveTransitiveClosure.fsti @@ -69,3 +69,15 @@ val closure_inversion: #a:Type u#a -> r:binrel u#a u#r a -> x:a -> y:a val stable_on_closure: #a:Type u#a -> r:binrel u#a u#r a -> p:(a -> Type0) -> p_stable_on_r: (squash (forall x y.{:pattern (p y); (r x y)} p x /\ squash (r x y) ==> p y)) -> Lemma (forall x y.{:pattern (closure r x y)} p x /\ closure r x y ==> p y) + +(** +* Induction over the reflective transitive closure of r +*) +val induct + (#a:Type) (r:binrel a) (p: a -> a -> prop) + (f_refl: (x:a -> squash (p x x))) + (f_step: (x:a -> y:a { r x y } -> squash (p x y))) + (f_closure: (x:a -> y:a -> z:a { p x y /\ p y z } -> squash (p x z))) + (x:a) (y:a) (xy:squash (closure r x y)) +: squash (p x y) +