Some experiments on a co-inductive Heityng algebra.

diff --git a/helm/software/matita/nlibrary/logic/cologic.ma b/helm/software/matita/nlibrary/logic/cologic.ma
new file mode 100644 (file)
index 0000000..474eab7
--- /dev/null
+++ b/helm/software/matita/nlibrary/logic/cologic.ma
@@ -0,0 +1,253 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/pts.ma".
+include "logic/equality.ma".
+
+ncoinductive cprop: Type[0] ≝
+   false: cprop
+ | true: cprop
+ | maybe: cprop → cprop.
+
+ntheorem ccases:
+ ∀c. c = match c with [ false ⇒ false | true ⇒ true | maybe c ⇒ maybe c ].
+ #c; ncases c; //.
+nqed.
+
+ninductive cconv : cprop → cprop → CProp[0] ≝
+   true_true: cconv true true
+ | false_false: cconv false false
+ | maybe1: ∀c1,c2. cconv c1 c2 → cconv (maybe c1) c2
+ | maybe2: ∀c1,c2. cconv c1 c2 → cconv c1 (maybe c2).
+
+ncoinductive cdiv: cprop → cprop → CProp[0] ≝
+   cdodiv: ∀c,d. cdiv c d → cdiv (maybe c) (maybe d).
+
+ndefinition cdiv1: ∀c. cdiv (maybe false) c → False.
+ #c K; ninversion K; #a b K1 K2 K3; ndestruct; ninversion K1; #; ndestruct.
+nqed.
+
+ndefinition cdiv2: ∀c. cdiv (maybe true) c → False.
+ #c K; ninversion K; #a b K1 K2 K3; ndestruct; ninversion K1; #; ndestruct.
+nqed.
+
+ndefinition cdiv3: ∀c. cdiv c false → False.
+ #c K; ninversion K; #; ndestruct.
+nqed.
+
+ndefinition cdiv4: ∀c. cdiv c true → False.
+ #c K; ninversion K; #; ndestruct.
+nqed.
+
+nlet corec cdiv5 c d (K: cdiv (maybe c) d) : cdiv c d ≝ ?.
+ ngeneralize in match K; ncases c
+  [ #E; ncases (cdiv1 … E)
+  | #E; ncases (cdiv2 … E)
+  | ncases d
+     [ #e E; ncases (cdiv3 … E)
+     | #e E; ncases (cdiv4 … E)
+     | #x y K1; @; napply cdiv5; ninversion K1; #; ndestruct; nassumption]##]
+nqed.
+
+nlemma cconv_cdiv_false: ∀c,d,e. cconv c e → cdiv c d → False.
+ #c d e K; nelim K
+  [##1,2: #U; ninversion U; #; ndestruct
+  |##*: /3/]
+nqed.    
+
+ndefinition ceq ≝ λc1,c2. cconv c1 c2 ∨ cdiv c1 c2.
+
+ndefinition committed ≝ λc. ceq c c.
+
+nrecord cval : Type[0] ≝ {
+   ccarr:> cprop;
+   ccomm: committed ccarr
+}.
+
+ntheorem ceq_refl: ∀c:cval. ceq c c.
+ //.
+nqed.
+
+nlet corec cdiv_sym c d (K: cdiv c d) : cdiv d c ≝ ?.
+ ncases K; /3/.
+nqed.
+
+nlet rec cconv_sym c d (K: cconv c d) on K : cconv d c ≝ ?.
+ ncases K; /3/.
+nqed.
+
+ntheorem ceq_sym: ∀c,d:cval. ceq c d → ceq d c.
+ #x; ncases x; #c Kc; #y; ncases y; #d Kd;
+ ncases Kc; #K1; *; /3/.
+nqed.
+      
+nlet corec cand c1 c2 : cprop ≝
+ match c1 with
+  [ false ⇒ false
+  | true ⇒ c2
+  | maybe c ⇒
+     match c2 with
+      [ false ⇒ false
+      | true ⇒ maybe c
+      | maybe d ⇒ maybe (cand c d) ]].
+
+nlemma cand_false: ∀c. cand false c = false.
+ #c; ncases c; nrewrite > (ccases (cand …)); //; #d;
+ nrewrite > (ccases (cand …)); //.
+nqed.
+
+nlemma cand_true: ∀c. cand true c = c.
+ #c; ncases c; nrewrite > (ccases (cand \ldots)); //; #d;
+ nrewrite > (ccases (cand …)); //.
+nqed.
+
+ntheorem cand_true: ∀c1,c2. ceq c1 true → ceq (cand c1 c2) c2.
+ #c1 c2 K; ncases K
+  [##2: #X; ncases (cdiv4 … X)
+  | #E; ninversion E (* induction inversion qui *)
+     [ #_; #_; nrewrite > (cand_true …); napply ceq_refl;
+     |
+ 
+
+ncoinductive cprop: Type[0] ≝
+   false: cprop
+ | true: cprop
+ | hmm: cprop → cprop.
+
+nlet corec cand c1 c2 : cprop ≝
+ match c1 with
+  [ false ⇒ false
+  | true ⇒ c2
+  | hmm c ⇒ hmm (cand c c2) ].
+
+nlet corec cor c1 c2 : cprop ≝
+ match c1 with
+  [ false ⇒ c2
+  | true ⇒ true
+  | hmm c ⇒ hmm (cor c c2) ].
+
+nlet corec cimpl c1 c2 : cprop ≝
+ match c2 with
+  [ false ⇒
+      match c1 with
+       [ false ⇒ true
+       | true ⇒ false
+       | hmm c ⇒ hmm (cimpl c c2) ]
+  | true ⇒ true
+  | hmm c ⇒ hmm (cimpl c1 c) ].
+
+include "Plogic/equality.ma".
+
+nlet corec ceq c1 c2 : cprop ≝
+ match c1 with
+  [ false ⇒
+     match c2 with
+      [ false ⇒ true
+      | true ⇒ false
+      | hmm c ⇒ hmm (ceq c1 c) ]
+  | true ⇒ c2
+  | hmm c ⇒ hmm (ceq c c2) ].
+
+ninductive holds: cprop → Prop ≝
+   holds_true: holds true
+ | holds_hmm: ∀c. holds c → holds (hmm c).
+
+include "Plogic/connectives.ma".
+
+nlemma ccases1:
+ ∀c. holds c →
+  match c with
+   [ true ⇒ True
+   | false ⇒ False
+   | hmm c' ⇒ holds c'].
+ #c; #H; ninversion H; //.
+nqed.
+
+nlemma ccases2:
+ ∀c.
+ match c with
+   [ true ⇒ True
+   | false ⇒ False
+   | hmm c' ⇒ holds c'] → holds c ≝ ?.
+ #c; ncases c; nnormalize; /2/; *.
+nqed.
+
+(*CSC: ??? *)
+naxiom cimpl1: ∀c. holds (cimpl true c) → holds c.
+
+nlemma ceq1: ∀c. holds c → holds (ceq c true).
+ #c H; nelim H; /2/.
+nqed.
+
+ncoinductive EQ: cprop → cprop → Prop ≝
+   EQ_true: EQ true true
+ | EQ_false: EQ false false
+ | EQ_hmm1: ∀x,y. EQ x y → EQ (hmm x) y
+ | EQ_hmm2: ∀x,y. EQ x y → EQ x (hmm y).
+
+naxiom daemon: False.
+
+nlet corec tech1 x: ∀y. EQ (hmm x) y → EQ x y ≝ ?.
+ #y; ncases y
+  [##1,2: #X; ninversion X; #; ndestruct; //
+  | #c; #X; ninversion X; #; ndestruct; //;
+    @4; ncases daemon (* napply tech1; //*) (* BUG GBC??? *)
+  ]
+nqed.
+
+nlemma Ccases1:
+ ∀c,d. EQ c d →
+  match c with
+   [ true ⇒ EQ true d
+   | false ⇒ EQ false d
+   | hmm c' ⇒ EQ c' d] ≝ ?.
+ #c d H; ninversion H; //;
+ #x y H H1 H2; ndestruct; ncases x in H ⊢ %; nnormalize; #; @4; //;
+ napply tech1; //.
+nqed.
+
+nlemma Ccases2:
+ ∀c,d.
+  match c with
+   [ true ⇒ EQ true d
+   | false ⇒ EQ false d
+   | hmm c' ⇒ EQ c' d] → EQ c d ≝ ?.
+ #c; ncases c; nnormalize; /2/.
+nqed.
+
+nlet corec heyting5 x: ∀y. EQ (cimpl (cand x y) x) true ≝ ?.
+ #y; napply Ccases2; ncases x; ncases y; nnormalize; /3/
+  [ #c; napply heyting5;
+
+
+nlemma heyting3: ∀x,y. holds (cimpl x (cimpl y x)).
+ #x; #y; ncases x; ncases y; /3/; nnormalize
+  [ #d; napply ccases2; nnormalize; napply ccases2; nnormalize; 
+
+nlemma heyting1: ∀x,y. holds (cimpl x y) → holds (cimpl y x) → holds (ceq x y).
+ #x y; #H; ngeneralize in match (refl … (cimpl x y));
+ nelim H in ⊢ (???% → % → %)
+  [ #K1; #K2; nrewrite > K1 in K2; #X1;    
+ 
+  napply ccases2; nlapply (ccases1 … H1); nlapply (ccases1 … H2);
+ ncases x; ncases y; nnormalize; /2/
+  [ #c; #H3 H4; nlapply (cimpl1 … H3); napply ceq1
+  | #d; #e; #H3; #H4;  
+
+ ncases x; nnormalize
+  [ #y; ncases y; //
+  | #y; ncases y; //
+     [ #H1; ninversion H1; ##[##1,4: #; ndestruct]
+       ##[ ncases (cimpl true false);
+    [ ninversion H1; #; ndestruct; 
\ No newline at end of file