From efc13d4e089923d7a9a7c4b8960469cc60f04ec9 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Wed, 6 Nov 2024 19:01:04 -0800
Subject: [PATCH] induction on reflexive transitive closure

---
 ulib/FStar.ReflexiveTransitiveClosure.fst  | 24 ++++++++++++++++++++++
 ulib/FStar.ReflexiveTransitiveClosure.fsti | 12 +++++++++++
 2 files changed, 36 insertions(+)

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)
+