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 "hints_declaration.ma".
16 include "sets/setoids1.ma".
18 ndefinition CPROP: setoid1.
21 | napply (mk_equivalence_relation1 CProp[0])
23 | #x; napply mk_iff; #H; nassumption
24 | #x; #y; *; #H1; #H2; napply mk_iff; nassumption
25 | #x; #y; #z; *; #H1; #H2; *; #H3; #H4; napply mk_iff; #w
26 [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
29 alias symbol "hint_decl" = "hint_decl_CProp2".
30 unification hint 0 ≔ ⊢ CProp[0] ≡ carr1 CPROP.
32 (*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
33 ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
34 on _x: carr1 CPROP to CProp[0].*)
36 alias symbol "eq" = "setoid1 eq".
38 ndefinition fi': ∀A,B:CPROP. A = B → B → A.
39 #A; #B; #H; napply (fi … H); nassumption.
42 notation ". r" with precedence 50 for @{'fi $r}.
43 interpretation "fi" 'fi r = (fi' ?? r).
45 ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
46 napply (mk_binary_morphism1 … And);
47 #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x; #y; @
48 [ napply (. Ha^-1) | napply (. Hb^-1) | napply (. Ha) | napply (. Hb)] //.
51 unification hint 0 ≔ A,B:CProp[0];
53 MM ≟ mk_unary_morphism1 …
54 (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
55 (prop11 … and_morphism)
56 (*-------------------------------------------------------------*) ⊢
57 fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ And A B.
62 nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
63 #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon.
70 ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
71 napply (mk_binary_morphism1 … Or);
72 #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x
73 [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
76 unification hint 0 ≔ A,B:CProp[0];
78 MM ≟ mk_unary_morphism1 …
79 (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
80 (prop11 … or_morphism)
81 (*-------------------------------------------------------------*) ⊢
82 fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
84 ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
85 napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
86 #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
87 [ napply (. Hb^-1); napply H; napply (. Ha) | napply (. Hb); napply H; napply (. Ha^-1)]
91 unification hint 0 ≔ A,B ⊢
93 (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
94 (prop11 … if_morphism)
98 nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
99 @(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
101 unification hint 0 ≔ P : CProp[0];
104 M ≟ mk_unary_morphism1 ?? (λP.¬ P) (prop11 ?? Not_morphism)
105 (*------------------------*)⊢
108 (* Ex setoid support *)
110 (* The caml, as some patches for it
111 ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
114 (* simple case where the whole predicate can be rewritten *)
115 nlemma Ex_morphism : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
116 #S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P);
117 #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
119 unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CProp[0];
120 A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
122 M ≟ mk_unary_morphism1 ?? (λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P)
123 (prop11 ?? (Ex_morphism S))
124 (*------------------------*)⊢
125 fun11 A B M P ≡ Ex S (fun11 (setoid1_of_setoid S) CPROP P).
127 nlemma Ex_morphism_eta : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
128 #S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x));
129 #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
131 unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CProp[0];
132 A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
134 M ≟ mk_unary_morphism1 ?? (λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x))
135 (prop11 ?? (Ex_morphism_eta S))
136 (*------------------------*)⊢
137 fun11 A B M P ≡ Ex S (λx.fun11 (setoid1_of_setoid S) CPROP P x).
139 nlemma Ex_setoid : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CPROP) → setoid.
140 #T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
142 unification hint 0 ≔ T,P ;
144 (*---------------------------*) ⊢
145 Ex T (λx:T.P x) ≡ carr S.
147 (* couts how many Ex we are traversing *)
148 ninductive counter : Type[0] ≝
150 | Next : (Prop → Prop) → (* dummy arg please the notation mechanism *)
153 (* to rewrite terms (live in setoid) *)
154 nlet rec mk_P (S, T : setoid) (n : counter) on n ≝
155 match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P S T m) ].
157 nlet rec mk_F (S, T : setoid) (n : counter) on n ≝
158 match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F S T m) ].
160 nlet rec mk_E (S, T : setoid) (n : counter) on n : ∀f,g : mk_F S T n. CProp[0] ≝
162 [ End ⇒ λf,g:T. f = g
163 | Next q m ⇒ λf,g: mk_F S T (Next q m). ∀x:S.mk_E S T m (f x) (g x) ].
165 nlet rec mk_H (S, T : setoid) (n : counter) on n :
166 ∀P1,P2: mk_P S T n.∀f,g : mk_F S T n. CProp[1] ≝
168 [ End ⇒ λP1,P2:mk_P S T End.λf,g:T. f = g → P1 f =_1 P2 g
169 | Next q m ⇒ λP1,P2: mk_P S T (Next q m).λf,g: mk_F S T (Next q m).
170 ∀x:S.mk_H S T m (P1 x) (P2 x) (f x) (g x) ].
172 nlet rec mk_Ex (S, T : setoid) (n : counter) on n :
173 ∀P: mk_P S T n.∀f : mk_F S T n. CProp[0] ≝
175 [ End ⇒ λP:mk_P S T End.λf:T. P f
176 | Next q m ⇒ λP: mk_P S T (Next q m).λf: mk_F S T (Next q m).
177 ∃x:S.mk_Ex S T m (P x) (f x) ].
179 nlemma Sig_generic : ∀S,T.∀n:counter.∀P,f,g.
180 mk_E S T n f g → mk_H S T n P P f g → mk_Ex S T n P f =_1 mk_Ex S T n P g.
181 #S T n; nelim n; nnormalize;
183 ##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
186 (* to rewrite propositions (live in setoid1) *)
187 nlet rec mk_P1 (S : setoid) (T : setoid1) (n : counter) on n ≝
188 match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P1 S T m) ].
190 nlet rec mk_F1 (S : setoid) (T : setoid1) (n : counter) on n ≝
191 match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F1 S T m) ].
193 nlet rec mk_E1 (S : setoid) (T : setoid1) (n : counter) on n : ∀f,g : mk_F1 S T n. CProp[1] ≝
195 [ End ⇒ λf,g:T. f =_1 g
196 | Next q m ⇒ λf,g: mk_F1 S T (Next q m). ∀x:S.mk_E1 S T m (f x) (g x) ].
198 nlet rec mk_H1 (S : setoid) (T : setoid1) (n : counter) on n :
199 ∀P1,P2: mk_P1 S T n.∀f,g : mk_F1 S T n. CProp[1] ≝
201 [ End ⇒ λP1,P2:mk_P1 S T End.λf,g:T. f = g → P1 f =_1 P2 g
202 | Next q m ⇒ λP1,P2: mk_P1 S T (Next q m).λf,g: mk_F1 S T (Next q m).
203 ∀x:S.mk_H1 S T m (P1 x) (P2 x) (f x) (g x) ].
205 nlet rec mk_Ex1 (S : setoid) (T : setoid1) (n : counter) on n :
206 ∀P: mk_P1 S T n.∀f : mk_F1 S T n. CProp[0] ≝
208 [ End ⇒ λP:mk_P1 S T End.λf:T. P f
209 | Next q m ⇒ λP: mk_P1 S T (Next q m).λf: mk_F1 S T (Next q m).
210 ∃x:S.mk_Ex1 S T m (P x) (f x) ].
212 nlemma Sig_generic1 : ∀S,T.∀n:counter.∀P,f,g.
213 mk_E1 S T n f g → mk_H1 S T n P P f g → mk_Ex1 S T n P f =_1 mk_Ex1 S T n P g.
214 #S T n; nelim n; nnormalize;
216 ##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
219 (* notation "∑x1,...,xn. E / H ; P" were:
220 - x1...xn are bound in E and P, H is bound in P
221 - H is an identifier that will have the type of E in P
222 - P is the proof that the two existentially quantified predicates are equal*)
223 notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20
225 ${ fold right @{ 'End } rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
226 ${ fold right @{ $E } rec acc @{ λ${ident x}.$acc } }
227 ${ fold right @{ λ${ident nE}.$H } rec acc @{ λ${ident x}.$acc } }
230 interpretation "next" 'Next x y = (Next x y).
231 interpretation "end" 'End = End.
232 interpretation "sig_gen" 'Sig_gen n E H = (Sig_generic ?? n ??? E H).
233 interpretation "sig_gen1" 'Sig_gen n E H = (Sig_generic1 ?? n ??? E H).
236 nlemma test0 : ∀S:setoid. ∀P: (setoid1_of_setoid S) ⇒_1 CPROP.∀f,g:S → S.
237 (∀x:S.f x = g x) → (Ex S (λw.P (f w))) =_1 (Ex S (λw.P (g w))).
238 #S P f g E; napply (∑w. E w / H ; ┼_1H); nqed.
240 nlemma test : ∀S:setoid. ∀P: (setoid1_of_setoid S) ⇒_1 CPROP.∀f,g:S → S.
241 (∀x:S.f x = g x) → (Ex S (λw.P (f w)∧ True)) =_1 (Ex S (λw.P (g w)∧ True)).
242 #S P f g E; napply (∑w. E w / H ; (┼_1H)╪_1#); nqed.
244 nlemma test_bound : ∀S:setoid. ∀e,f: (setoid1_of_setoid S) ⇒_1 CPROP. e = f →
245 (Ex S (λw.e w ∧ True)) =_1 (Ex S (λw.f w ∧ True)).
246 #S f g E; napply (.=_1 ∑x. E x x # / H ; (H ╪_1 #)); //; nqed.
248 nlemma test2 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoid S) ⇒_1 CPROP.
249 ∀x,y:setoid1_of_setoid S.x =_1 y →
250 (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
251 #S m x y E; napply (.=_1 #╪_1(∑w. E / E ; ((E ╪_1 #) ╪_1 #))). //; nqed.
253 nlemma test3 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoid S) ⇒_1 CPROP.
254 ∀x,y:setoid1_of_setoid S.x =_1 y →
255 ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
256 #S m x y E; napply (.=_1 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.