1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/pts.ma".
16 include "logic/equality.ma".
17 include "datatypes/bool.ma".
19 ncoinductive cprop: Type[0] ≝
21 | maybe: cprop → cprop.
24 ∀c. c = match c with [ certain b ⇒ certain b | maybe c ⇒ maybe c ].
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).
33 nlemma cconv_sym: ∀c,d. cconv c d → cconv d c.
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).
42 nlet corec ceq_refl c : ceq c c ≝ ?.
43 ncases c [ #b; @2; @1 | #d; @1; //]
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/.
52 nlemma ceq_to_cconv: ∀c,b. ceq c (certain b) → cconv c (certain b).
53 #c b K; ninversion K; #; ndestruct; //.
56 nlemma ceq_to_cconv2: ∀c,b. ceq (certain b) c → cconv (certain b) c.
57 #c b K; ninversion K; #; ndestruct; //.
60 nlet corec cand c1 c2 : cprop ≝
62 [ certain b ⇒ match b with [ false ⇒ certain false | true ⇒ c2 ]
65 [ certain b ⇒ match b with [ false ⇒ certain false | true ⇒ maybe c ]
66 | maybe d ⇒ maybe (cand c d) ]].
68 nlemma cand_false: ∀c. cand (certain false) c = certain false.
69 #c; ncases c; nrewrite > (ccases (cand …)); //; #d;
70 nrewrite > (ccases (cand …)); //.
73 nlemma cand_true: ∀c. cand (certain true) c = c.
74 #c; ncases c; nrewrite > (ccases (cand …)); //; #d;
75 nrewrite > (ccases (cand …)); //.
78 nlemma cand_truer: ∀c. cand c (certain true) = c.
81 | #d; nrewrite > (ccases (cand …)); // ]
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);
89 | nrewrite < E3 in E1; #K1;
90 ncut (∀y,z. cconv y z → z = certain true → ceq (cand y c2) c2); /2/;
92 [ #e E; nrewrite > E; nrewrite > (cand_true c2); //
94 [ #bb; ncases bb; #xx yy KK1 KK2 EE;
95 ##[ nlapply (KK2 EE); #XX; nrewrite > (cand_truer …) in XX; #YY;
98 rewrite > (ccases (cand (maybe xx) (certain true)));
103 ncoinductive cprop: Type[0] ≝
106 | hmm: cprop → cprop.
108 nlet corec cand c1 c2 : cprop ≝
112 | hmm c ⇒ hmm (cand c c2) ].
114 nlet corec cor c1 c2 : cprop ≝
118 | hmm c ⇒ hmm (cor c c2) ].
120 nlet corec cimpl c1 c2 : cprop ≝
126 | hmm c ⇒ hmm (cimpl c c2) ]
128 | hmm c ⇒ hmm (cimpl c1 c) ].
130 include "Plogic/equality.ma".
132 nlet corec ceq c1 c2 : cprop ≝
138 | hmm c ⇒ hmm (ceq c1 c) ]
140 | hmm c ⇒ hmm (ceq c c2) ].
142 ninductive holds: cprop → Prop ≝
143 holds_true: holds true
144 | holds_hmm: ∀c. holds c → holds (hmm c).
146 include "Plogic/connectives.ma".
153 | hmm c' ⇒ holds c'].
154 #c; #H; ninversion H; //.
162 | hmm c' ⇒ holds c'] → holds c ≝ ?.
163 #c; ncases c; nnormalize; /2/; *.
167 naxiom cimpl1: ∀c. holds (cimpl true c) → holds c.
169 nlemma ceq1: ∀c. holds c → holds (ceq c true).
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).
179 naxiom daemon: False.
181 nlet corec tech1 x: ∀y. EQ (hmm x) y → EQ x y ≝ ?.
183 [##1,2: #X; ninversion X; #; ndestruct; //
184 | #c; #X; ninversion X; #; ndestruct; //;
185 @4; ncases daemon (* napply tech1; //*) (* BUG GBC??? *)
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; //;
205 | hmm c' ⇒ EQ c' d] → EQ c d ≝ ?.
206 #c; ncases c; nnormalize; /2/.
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;
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;
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;
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
231 [ #H1; ninversion H1; ##[##1,4: #; ndestruct]
232 ##[ ncases (cimpl true false);
233 [ ninversion H1; #; ndestruct;