helm/software/matita/nlibrary/logic/cologic.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/pts.ma".
  16 include "logic/equality.ma".
  17
  18 ncoinductive cprop: Type[0] ≝
  19    false: cprop
  20  | true: cprop
  21  | maybe: cprop → cprop.
  22
  23 ntheorem ccases:
  24  ∀c. c = match c with [ false ⇒ false | true ⇒ true | maybe c ⇒ maybe c ].
  25  #c; ncases c; //.
  26 nqed.
  27
  28 ninductive cconv : cprop → cprop → CProp[0] ≝
  29    true_true: cconv true true
  30  | false_false: cconv false false
  31  | maybe1: ∀c1,c2. cconv c1 c2 → cconv (maybe c1) c2
  32  | maybe2: ∀c1,c2. cconv c1 c2 → cconv c1 (maybe c2).
  33
  34 ncoinductive cdiv: cprop → cprop → CProp[0] ≝
  35    cdodiv: ∀c,d. cdiv c d → cdiv (maybe c) (maybe d).
  36
  37 ndefinition cdiv1: ∀c. cdiv (maybe false) c → False.
  38  #c K; ninversion K; #a b K1 K2 K3; ndestruct; ninversion K1; #; ndestruct.
  39 nqed.
  40
  41 ndefinition cdiv2: ∀c. cdiv (maybe true) c → False.
  42  #c K; ninversion K; #a b K1 K2 K3; ndestruct; ninversion K1; #; ndestruct.
  43 nqed.
  44
  45 ndefinition cdiv3: ∀c. cdiv c false → False.
  46  #c K; ninversion K; #; ndestruct.
  47 nqed.
  48
  49 ndefinition cdiv4: ∀c. cdiv c true → False.
  50  #c K; ninversion K; #; ndestruct.
  51 nqed.
  52
  53 nlet corec cdiv5 c d (K: cdiv (maybe c) d) : cdiv c d ≝ ?.
  54  ngeneralize in match K; ncases c
  55   [ #E; ncases (cdiv1 … E)
  56   | #E; ncases (cdiv2 … E)
  57   | ncases d
  58      [ #e E; ncases (cdiv3 … E)
  59      | #e E; ncases (cdiv4 … E)
  60      | #x y K1; @; napply cdiv5; ninversion K1; #; ndestruct; nassumption]##]
  61 nqed.
  62
  63 nlemma cconv_cdiv_false: ∀c,d,e. cconv c e → cdiv c d → False.
  64  #c d e K; nelim K
  65   [##1,2: #U; ninversion U; #; ndestruct
  66   |##*: /3/]
  67 nqed.
  68
  69 ndefinition ceq ≝ λc1,c2. cconv c1 c2 ∨ cdiv c1 c2.
  70
  71 ndefinition committed ≝ λc. ceq c c.
  72
  73 nrecord cval : Type[0] ≝ {
  74    ccarr:> cprop;
  75    ccomm: committed ccarr
  76 }.
  77
  78 ntheorem ceq_refl: ∀c:cval. ceq c c.
  79  //.
  80 nqed.
  81
  82 nlet corec cdiv_sym c d (K: cdiv c d) : cdiv d c ≝ ?.
  83  ncases K; /3/.
  84 nqed.
  85
  86 nlet rec cconv_sym c d (K: cconv c d) on K : cconv d c ≝ ?.
  87  ncases K; /3/.
  88 nqed.
  89
  90 ntheorem ceq_sym: ∀c,d:cval. ceq c d → ceq d c.
  91  #x; ncases x; #c Kc; #y; ncases y; #d Kd;
  92  ncases Kc; #K1; *; /3/.
  93 nqed.
  94
  95 nlet corec cand c1 c2 : cprop ≝
  96  match c1 with
  97   [ false ⇒ false
  98   | true ⇒ c2
  99   | maybe c ⇒
 100      match c2 with
 101       [ false ⇒ false
 102       | true ⇒ maybe c
 103       | maybe d ⇒ maybe (cand c d) ]].
 104
 105 nlemma cand_false: ∀c. cand false c = false.
 106  #c; ncases c; nrewrite > (ccases (cand …)); //; #d;
 107  nrewrite > (ccases (cand …)); //.
 108 nqed.
 109
 110 nlemma cand_true: ∀c. cand true c = c.
 111  #c; ncases c; nrewrite > (ccases (cand \ldots)); //; #d;
 112  nrewrite > (ccases (cand …)); //.
 113 nqed.
 114
 115 ntheorem cand_true: ∀c1,c2. ceq c1 true → ceq (cand c1 c2) c2.
 116  #c1 c2 K; ncases K
 117   [##2: #X; ncases (cdiv4 … X)
 118   | #E; ninversion E (* induction inversion qui *)
 119      [ #_; #_; nrewrite > (cand_true …); napply ceq_refl;
 120      |
 121
 122
 123 ncoinductive cprop: Type[0] ≝
 124    false: cprop
 125  | true: cprop
 126  | hmm: cprop → cprop.
 127
 128 nlet corec cand c1 c2 : cprop ≝
 129  match c1 with
 130   [ false ⇒ false
 131   | true ⇒ c2
 132   | hmm c ⇒ hmm (cand c c2) ].
 133
 134 nlet corec cor c1 c2 : cprop ≝
 135  match c1 with
 136   [ false ⇒ c2
 137   | true ⇒ true
 138   | hmm c ⇒ hmm (cor c c2) ].
 139
 140 nlet corec cimpl c1 c2 : cprop ≝
 141  match c2 with
 142   [ false ⇒
 143       match c1 with
 144        [ false ⇒ true
 145        | true ⇒ false
 146        | hmm c ⇒ hmm (cimpl c c2) ]
 147   | true ⇒ true
 148   | hmm c ⇒ hmm (cimpl c1 c) ].
 149
 150 include "Plogic/equality.ma".
 151
 152 nlet corec ceq c1 c2 : cprop ≝
 153  match c1 with
 154   [ false ⇒
 155      match c2 with
 156       [ false ⇒ true
 157       | true ⇒ false
 158       | hmm c ⇒ hmm (ceq c1 c) ]
 159   | true ⇒ c2
 160   | hmm c ⇒ hmm (ceq c c2) ].
 161
 162 ninductive holds: cprop → Prop ≝
 163    holds_true: holds true
 164  | holds_hmm: ∀c. holds c → holds (hmm c).
 165
 166 include "Plogic/connectives.ma".
 167
 168 nlemma ccases1:
 169  ∀c. holds c →
 170   match c with
 171    [ true ⇒ True
 172    | false ⇒ False
 173    | hmm c' ⇒ holds c'].
 174  #c; #H; ninversion H; //.
 175 nqed.
 176
 177 nlemma ccases2:
 178  ∀c.
 179  match c with
 180    [ true ⇒ True
 181    | false ⇒ False
 182    | hmm c' ⇒ holds c'] → holds c ≝ ?.
 183  #c; ncases c; nnormalize; /2/; *.
 184 nqed.
 185
 186 (*CSC: ??? *)
 187 naxiom cimpl1: ∀c. holds (cimpl true c) → holds c.
 188
 189 nlemma ceq1: ∀c. holds c → holds (ceq c true).
 190  #c H; nelim H; /2/.
 191 nqed.
 192
 193 ncoinductive EQ: cprop → cprop → Prop ≝
 194    EQ_true: EQ true true
 195  | EQ_false: EQ false false
 196  | EQ_hmm1: ∀x,y. EQ x y → EQ (hmm x) y
 197  | EQ_hmm2: ∀x,y. EQ x y → EQ x (hmm y).
 198
 199 naxiom daemon: False.
 200
 201 nlet corec tech1 x: ∀y. EQ (hmm x) y → EQ x y ≝ ?.
 202  #y; ncases y
 203   [##1,2: #X; ninversion X; #; ndestruct; //
 204   | #c; #X; ninversion X; #; ndestruct; //;
 205     @4; ncases daemon (* napply tech1; //*) (* BUG GBC??? *)
 206   ]
 207 nqed.
 208
 209 nlemma Ccases1:
 210  ∀c,d. EQ c d →
 211   match c with
 212    [ true ⇒ EQ true d
 213    | false ⇒ EQ false d
 214    | hmm c' ⇒ EQ c' d] ≝ ?.
 215  #c d H; ninversion H; //;
 216  #x y H H1 H2; ndestruct; ncases x in H ⊢ %; nnormalize; #; @4; //;
 217  napply tech1; //.
 218 nqed.
 219
 220 nlemma Ccases2:
 221  ∀c,d.
 222   match c with
 223    [ true ⇒ EQ true d
 224    | false ⇒ EQ false d
 225    | hmm c' ⇒ EQ c' d] → EQ c d ≝ ?.
 226  #c; ncases c; nnormalize; /2/.
 227 nqed.
 228
 229 nlet corec heyting5 x: ∀y. EQ (cimpl (cand x y) x) true ≝ ?.
 230  #y; napply Ccases2; ncases x; ncases y; nnormalize; /3/
 231   [ #c; napply heyting5;
 232
 233
 234 nlemma heyting3: ∀x,y. holds (cimpl x (cimpl y x)).
 235  #x; #y; ncases x; ncases y; /3/; nnormalize
 236   [ #d; napply ccases2; nnormalize; napply ccases2; nnormalize;
 237
 238 nlemma heyting1: ∀x,y. holds (cimpl x y) → holds (cimpl y x) → holds (ceq x y).
 239  #x y; #H; ngeneralize in match (refl … (cimpl x y));
 240  nelim H in ⊢ (???% → % → %)
 241   [ #K1; #K2; nrewrite > K1 in K2; #X1;
 242
 243   napply ccases2; nlapply (ccases1 … H1); nlapply (ccases1 … H2);
 244  ncases x; ncases y; nnormalize; /2/
 245   [ #c; #H3 H4; nlapply (cimpl1 … H3); napply ceq1
 246   | #d; #e; #H3; #H4;
 247
 248  ncases x; nnormalize
 249   [ #y; ncases y; //
 250   | #y; ncases y; //
 251      [ #H1; ninversion H1; ##[##1,4: #; ndestruct]
 252        ##[ ncases (cimpl true false);
 253     [ ninversion H1; #; ndestruct;