X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fcologic.ma;h=8b9ed3c15d450c622d78eb42294f43a98d145922;hb=bf7be462a06e739b39af20f72362857e849a2aa0;hp=474eab7267108b691369e444d6d49faf64e29dbd;hpb=d8ab88f926134731baa64f48c519289587c20261;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/cologic.ma b/helm/software/matita/nlibrary/logic/cologic.ma
index 474eab726..8b9ed3c15 100644
--- a/helm/software/matita/nlibrary/logic/cologic.ma
+++ b/helm/software/matita/nlibrary/logic/cologic.ma
@@ -14,110 +14,90 @@
 
 include "logic/pts.ma".
 include "logic/equality.ma".
+include "datatypes/bool.ma".
 
 ncoinductive cprop: Type[0] ≝
-   false: cprop
- | true: cprop
+   certain: bool → cprop
  | maybe: cprop → cprop.
 
 ntheorem ccases:
- ∀c. c = match c with [ false ⇒ false | true ⇒ true | maybe c ⇒ maybe c ].
+ ∀c. c = match c with [ certain b ⇒ certain b | maybe c ⇒ maybe c ].
  #c; ncases c; //.
 nqed.
 
 ninductive cconv : cprop → cprop → CProp[0] ≝
-   true_true: cconv true true
- | false_false: cconv false false
+   certain_certain: ∀b. cconv b b
  | 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.
+nlemma cconv_sym: ∀c,d. cconv c d → cconv d c.
+ #c d K; nelim K; /2/.
 nqed.
 
-ndefinition cdiv2: ∀c. cdiv (maybe true) c → False.
- #c K; ninversion K; #a b K1 K2 K3; ndestruct; ninversion K1; #; ndestruct.
-nqed.
+ncoinductive ceq: cprop → cprop → CProp[0] ≝
+   maybe_maybe: ∀c,d. ceq c d → ceq (maybe c) (maybe d)
+ | certain_maybe: ∀b,c. cconv (certain b) c → ceq (certain b) c
+ | maybe_certain: ∀b,c. cconv c (certain b) → ceq c (certain b).
 
-ndefinition cdiv3: ∀c. cdiv c false → False.
- #c K; ninversion K; #; ndestruct.
+nlet corec ceq_refl c : ceq c c ≝ ?.
+ ncases c [ #b; @2; @1 | #d; @1; //]
 nqed.
 
-ndefinition cdiv4: ∀c. cdiv c true → False.
- #c K; ninversion K; #; ndestruct.
+nlet corec ceq_sym c d : ceq c d → ceq d c ≝ ?.
+ ncases c; ncases d; #x y K; ninversion K; #a b E1 E2 E3
+ [##4,10: @1; napply ceq_sym; napply E1]
+ ndestruct [ @2 | @2 | @3 | @2] /2/.
 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]##]
+nlemma ceq_to_cconv: ∀c,b. ceq c (certain b) → cconv c (certain b).
+ #c b K; ninversion K; #; ndestruct; //.
 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/.
+nlemma ceq_to_cconv2: ∀c,b. ceq (certain b) c → cconv (certain b) c.
+ #c b K; ninversion K; #; ndestruct; //.
 nqed.
       
 nlet corec cand c1 c2 : cprop ≝
  match c1 with
-  [ false ⇒ false
-  | true ⇒ c2
+  [ certain b ⇒ match b with [ false ⇒ certain false | true ⇒ c2 ]
   | maybe c ⇒
      match c2 with
-      [ false ⇒ false
-      | true ⇒ maybe c
+      [ certain b ⇒ match b with [ false ⇒ certain false | true ⇒ maybe c ]
       | maybe d ⇒ maybe (cand c d) ]].
 
-nlemma cand_false: ∀c. cand false c = false.
+nlemma cand_false: ∀c. cand (certain false) c = certain 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;
+nlemma cand_true: ∀c. cand (certain true) c = c.
+ #c; ncases c; nrewrite > (ccases (cand …)); //; #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;
-     |
+nlemma cand_truer: ∀c. cand c (certain true) = c.
+ #c; ncases c
+  [ #b; ncases b; //
+  | #d; nrewrite > (ccases (cand …)); // ]
+nqed.
+
+
+ntheorem cand_true: ∀c1,c2. ceq c1 (certain true) → ceq (cand c1 c2) c2.
+ #c1 c2 K; ninversion K; #x y E1 E2 E3 [ ndestruct ]
+ ##[ nrewrite < E3 in E1; #K1; ninversion K1; #; ndestruct; nrewrite > (cand_true c2);
+     //
+   | nrewrite < E3 in E1; #K1;
+     ncut (∀y,z. cconv y z → z = certain true → ceq (cand y c2) c2); /2/;
+     #a b X; nelim X
+      [ #e E; nrewrite > E; nrewrite > (cand_true c2); //
+      | ncases c2
+         [ #bb; ncases bb; #xx yy KK1 KK2 EE;
+           ##[ nlapply (KK2 EE); #XX; nrewrite > (cand_truer …) in XX; #YY;
+               @3;
+               
+           rewrite > (ccases (cand (maybe xx) (certain true)));
+               nnormalize; @3; @2; 
+
  
 
 ncoinductive cprop: Type[0] ≝