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 include "datatypes/bool.ma".
  18
  19 ncoinductive cprop: Type[0] ≝
  20    certain: bool → cprop
  21  | maybe: cprop → cprop.
  22
  23 ntheorem ccases:
  24  ∀c. c = match c with [ certain b ⇒ certain b | maybe c ⇒ maybe c ].
  25  #c; ncases c; //.
  26 nqed.
  27
  28 ninductive cconv : cprop → cprop → CProp[0] ≝
  29    certain_certain: ∀b. cconv b b
  30  | maybe1: ∀c1,c2. cconv c1 c2 → cconv (maybe c1) c2
  31  | maybe2: ∀c1,c2. cconv c1 c2 → cconv c1 (maybe c2).
  32
  33 nlemma cconv_sym: ∀c,d. cconv c d → cconv d c.
  34  #c d K; nelim K; /2/.
  35 nqed.
  36
  37 ncoinductive ceq: cprop → cprop → CProp[0] ≝
  38    maybe_maybe: ∀c,d. ceq c d → ceq (maybe c) (maybe d)
  39  | certain_maybe: ∀b,c. cconv (certain b) c → ceq (certain b) c
  40  | maybe_certain: ∀b,c. cconv c (certain b) → ceq c (certain b).
  41
  42 nlet corec ceq_refl c : ceq c c ≝ ?.
  43  ncases c [ #b; @2; @1 | #d; @1; //]
  44 nqed.
  45
  46 nlet corec ceq_sym c d : ceq c d → ceq d c ≝ ?.
  47  ncases c; ncases d; #x y K; ninversion K; #a b E1 E2 E3
  48  [##4,10: @1; napply ceq_sym; napply E1]
  49  ndestruct [ @2 | @2 | @3 | @2] /2/.
  50 nqed.
  51
  52 nlemma ceq_to_cconv: ∀c,b. ceq c (certain b) → cconv c (certain b).
  53  #c b K; ninversion K; #; ndestruct; //.
  54 nqed.
  55
  56 nlemma ceq_to_cconv2: ∀c,b. ceq (certain b) c → cconv (certain b) c.
  57  #c b K; ninversion K; #; ndestruct; //.
  58 nqed.
  59
  60 nlet corec cand c1 c2 : cprop ≝
  61  match c1 with
  62   [ certain b ⇒ match b with [ false ⇒ certain false | true ⇒ c2 ]
  63   | maybe c ⇒
  64      match c2 with
  65       [ certain b ⇒ match b with [ false ⇒ certain false | true ⇒ maybe c ]
  66       | maybe d ⇒ maybe (cand c d) ]].
  67
  68 nlemma cand_false: ∀c. cand (certain false) c = certain false.
  69  #c; ncases c; nrewrite > (ccases (cand …)); //; #d;
  70  nrewrite > (ccases (cand …)); //.
  71 nqed.
  72
  73 nlemma cand_true: ∀c. cand (certain true) c = c.
  74  #c; ncases c; nrewrite > (ccases (cand …)); //; #d;
  75  nrewrite > (ccases (cand …)); //.
  76 nqed.
  77
  78 nlemma cand_truer: ∀c. cand c (certain true) = c.
  79  #c; ncases c
  80   [ #b; ncases b; //
  81   | #d; nrewrite > (ccases (cand …)); // ]
  82 nqed.
  83
  84
  85 ntheorem cand_true: ∀c1,c2. ceq c1 (certain true) → ceq (cand c1 c2) c2.
  86  #c1 c2 K; ninversion K; #x y E1 E2 E3 [ ndestruct ]
  87  ##[ nrewrite < E3 in E1; #K1; ninversion K1; #; ndestruct; nrewrite > (cand_true c2);
  88      //
  89    | nrewrite < E3 in E1; #K1;
  90      ncut (∀y,z. cconv y z → z = certain true → ceq (cand y c2) c2); /2/;
  91      #a b X; nelim X
  92       [ #e E; nrewrite > E; nrewrite > (cand_true c2); //
  93       | ncases c2
  94          [ #bb; ncases bb; #xx yy KK1 KK2 EE;
  95            ##[ nlapply (KK2 EE); #XX; nrewrite > (cand_truer …) in XX; #YY;
  96                @3;
  97
  98            rewrite > (ccases (cand (maybe xx) (certain true)));
  99                nnormalize; @3; @2;
 100
 101
 102
 103 ncoinductive cprop: Type[0] ≝
 104    false: cprop
 105  | true: cprop
 106  | hmm: cprop → cprop.
 107
 108 nlet corec cand c1 c2 : cprop ≝
 109  match c1 with
 110   [ false ⇒ false
 111   | true ⇒ c2
 112   | hmm c ⇒ hmm (cand c c2) ].
 113
 114 nlet corec cor c1 c2 : cprop ≝
 115  match c1 with
 116   [ false ⇒ c2
 117   | true ⇒ true
 118   | hmm c ⇒ hmm (cor c c2) ].
 119
 120 nlet corec cimpl c1 c2 : cprop ≝
 121  match c2 with
 122   [ false ⇒
 123       match c1 with
 124        [ false ⇒ true
 125        | true ⇒ false
 126        | hmm c ⇒ hmm (cimpl c c2) ]
 127   | true ⇒ true
 128   | hmm c ⇒ hmm (cimpl c1 c) ].
 129
 130 include "Plogic/equality.ma".
 131
 132 nlet corec ceq c1 c2 : cprop ≝
 133  match c1 with
 134   [ false ⇒
 135      match c2 with
 136       [ false ⇒ true
 137       | true ⇒ false
 138       | hmm c ⇒ hmm (ceq c1 c) ]
 139   | true ⇒ c2
 140   | hmm c ⇒ hmm (ceq c c2) ].
 141
 142 ninductive holds: cprop → Prop ≝
 143    holds_true: holds true
 144  | holds_hmm: ∀c. holds c → holds (hmm c).
 145
 146 include "Plogic/connectives.ma".
 147
 148 nlemma ccases1:
 149  ∀c. holds c →
 150   match c with
 151    [ true ⇒ True
 152    | false ⇒ False
 153    | hmm c' ⇒ holds c'].
 154  #c; #H; ninversion H; //.
 155 nqed.
 156
 157 nlemma ccases2:
 158  ∀c.
 159  match c with
 160    [ true ⇒ True
 161    | false ⇒ False
 162    | hmm c' ⇒ holds c'] → holds c ≝ ?.
 163  #c; ncases c; nnormalize; /2/; *.
 164 nqed.
 165
 166 (*CSC: ??? *)
 167 naxiom cimpl1: ∀c. holds (cimpl true c) → holds c.
 168
 169 nlemma ceq1: ∀c. holds c → holds (ceq c true).
 170  #c H; nelim H; /2/.
 171 nqed.
 172
 173 ncoinductive EQ: cprop → cprop → Prop ≝
 174    EQ_true: EQ true true
 175  | EQ_false: EQ false false
 176  | EQ_hmm1: ∀x,y. EQ x y → EQ (hmm x) y
 177  | EQ_hmm2: ∀x,y. EQ x y → EQ x (hmm y).
 178
 179 naxiom daemon: False.
 180
 181 nlet corec tech1 x: ∀y. EQ (hmm x) y → EQ x y ≝ ?.
 182  #y; ncases y
 183   [##1,2: #X; ninversion X; #; ndestruct; //
 184   | #c; #X; ninversion X; #; ndestruct; //;
 185     @4; ncases daemon (* napply tech1; //*) (* BUG GBC??? *)
 186   ]
 187 nqed.
 188
 189 nlemma Ccases1:
 190  ∀c,d. EQ c d →
 191   match c with
 192    [ true ⇒ EQ true d
 193    | false ⇒ EQ false d
 194    | hmm c' ⇒ EQ c' d] ≝ ?.
 195  #c d H; ninversion H; //;
 196  #x y H H1 H2; ndestruct; ncases x in H ⊢ %; nnormalize; #; @4; //;
 197  napply tech1; //.
 198 nqed.
 199
 200 nlemma Ccases2:
 201  ∀c,d.
 202   match c with
 203    [ true ⇒ EQ true d
 204    | false ⇒ EQ false d
 205    | hmm c' ⇒ EQ c' d] → EQ c d ≝ ?.
 206  #c; ncases c; nnormalize; /2/.
 207 nqed.
 208
 209 nlet corec heyting5 x: ∀y. EQ (cimpl (cand x y) x) true ≝ ?.
 210  #y; napply Ccases2; ncases x; ncases y; nnormalize; /3/
 211   [ #c; napply heyting5;
 212
 213
 214 nlemma heyting3: ∀x,y. holds (cimpl x (cimpl y x)).
 215  #x; #y; ncases x; ncases y; /3/; nnormalize
 216   [ #d; napply ccases2; nnormalize; napply ccases2; nnormalize;
 217
 218 nlemma heyting1: ∀x,y. holds (cimpl x y) → holds (cimpl y x) → holds (ceq x y).
 219  #x y; #H; ngeneralize in match (refl … (cimpl x y));
 220  nelim H in ⊢ (???% → % → %)
 221   [ #K1; #K2; nrewrite > K1 in K2; #X1;
 222
 223   napply ccases2; nlapply (ccases1 … H1); nlapply (ccases1 … H2);
 224  ncases x; ncases y; nnormalize; /2/
 225   [ #c; #H3 H4; nlapply (cimpl1 … H3); napply ceq1
 226   | #d; #e; #H3; #H4;
 227
 228  ncases x; nnormalize
 229   [ #y; ncases y; //
 230   | #y; ncases y; //
 231      [ #H1; ninversion H1; ##[##1,4: #; ndestruct]
 232        ##[ ncases (cimpl true false);
 233     [ ninversion H1; #; ndestruct;