coinduction is between us

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index 0e4225d9650ed5baf0116e8a21c046a6329356ef..c33dca9bda95bbc30e53c94c9c901f7ada652869 100644 (file)
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -286,10 +286,50 @@ nlet rec move_star S w E on w ≝
 
 ndefinition in_moves ≝ λS,w,E. fst … (move_star S w E).
 
+ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
+ mk_equiv:
+  ∀E1,E2: bool × (pre S).
+   fst ?? E1  = fst ?? E2 →
+    (∀x. equiv S (move S x (snd … E1)) (move S x (snd … E2))) →
+     equiv S E1 E2.
+
 ndefinition NAT: decidable.
  @ nat eqb; /2/.
 nqed.
 
+ninductive unit: Type[0] ≝ I: unit.
+
+nlet corec foo_nop (b: bool):
+ equiv NAT
+  〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
+  〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
+ @; //; #x; ncases x
+  [ nnormalize in ⊢ (??%%); napply (foo_nop false)
+  | #y; ncases y
+     [ nnormalize in ⊢ (??%%); napply (foo_nop false)
+     | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
+nqed.
+
+nlet corec foo (a: unit):
+ equiv NAT
+  (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
+  (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
+≝ ?.
+ @;
+  ##[ nnormalize; //
+  ##| #x; ncases x
+       [ nnormalize in ⊢ (??%%);
+         nnormalize in foo: (? → ??%%);
+         @; //; #y; ncases y
+           [ nnormalize in ⊢ (??%%); napply foo_nop
+           | #y; ncases y
+              [ nnormalize in ⊢ (??%%);
+                
+            ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
+     ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
+  ##]
+nqed.
+
 ndefinition test1 ≝
  pc ? (pk ? (po ? (ps ? 0) (ps ? 1))) (ps ? 0).