From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 5 May 2010 15:13:41 +0000 (+0000)
Subject: coinduction is between us
X-Git-Tag: make_still_working~2913
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63b1b044e54bac3ffecc02ee2941b60f58b0c837;p=helm.git

coinduction is between us
---

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index 0e4225d96..c33dca9bd 100644
--- 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).