]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ICC/lamla.ma
- paths and left residuals: second case of the equivalence proved!
[helm.git] / matita / matita / contribs / ICC / lamla.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 "nat/compare.ma".
16 include "nat/plus.ma".
17 include "list/list.ma".
18
19 notation > "'if' term 19 E 'then' term 19 T 'else' term 19 F 'fi'" 
20 non associative with precedence 90
21 for @{ match $E with [ true ⇒ $T | false ⇒ $F ] }.
22
23 inductive PT : Type ≝ 
24   | Var : nat → PT
25   | Lam : PT → PT
26   | Appl : PT → PT → PT
27   | Bang : PT → PT
28   | Sect : PT → PT
29   | LetB : PT → PT → PT
30   | LetS : PT → PT → PT.
31
32 variant appl : PT → PT → PT ≝ Appl.
33 coercion appl 1.  
34   
35 notation > "! term 90 t" non associative with precedence 90 for @{ 'bang $t }.
36 notation < "! term 90 t" non associative with precedence 90 for @{ 'bang $t }.
37 interpretation "bang" 'bang t = (Bang t). 
38 notation > "§ t" non associative with precedence 90 for @{ 'sect $t }.
39 notation < "§ t" non associative with precedence 90 for @{ 'sect $t }.
40 interpretation "sect" 'sect t = (Sect t).
41 notation > "Λ t" non associative with precedence 90 for @{ 'lam $t }.
42 notation < "Λ t" non associative with precedence 90 for @{ 'lam $t }.
43 interpretation "lam" 'lam t = (Lam t).
44 notation < "Λ \sup ! t" non associative with precedence 90 for @{ 'lamb $t}.
45 notation > "*Λ t" non associative with precedence 90 for @{ 'lamb $t}.
46 interpretation "lamb" 'lamb t = (Lam (LetB (Var (S O)) t)).
47 notation "𝟙" non associative with precedence 90 for @{ 'one }.
48 interpretation "one" 'one = (Var (S O)).  
49 notation "𝟚" non associative with precedence 90 for @{ 'two }.
50 interpretation "two" 'two = (Var (S (S O))).  
51 notation "𝟛" non associative with precedence 90 for @{ 'three }.
52 interpretation "three" 'three = (Var (S (S (S O)))).  
53 notation "𝟜" non associative with precedence 90 for @{ 'four }.
54 interpretation "four" 'four = (Var (S (S (S (S O))))).  
55 notation < "a ­b" left associative with precedence 65 for @{ 'appl $a $b }.  
56 interpretation "appl" 'appl a b = (Appl a b).
57   
58 let rec lift (from:nat) (amount:nat) (what:PT) on what : PT ≝ 
59   match what with
60   [ Var n ⇒ if leb from n then Var (n+amount) else what fi
61   | Lam t ⇒ Lam (lift (1+from) amount t)
62   | Appl t1 t2 ⇒ Appl (lift from amount t1) (lift from amount t2)
63   | Bang t ⇒ Bang (lift from amount t)
64   | Sect t ⇒ Sect (lift from amount t)
65   | LetB t1 t2 ⇒ LetB (lift from amount t1) (lift (1+from) amount t2) 
66   | LetS t1 t2 ⇒ LetS (lift from amount t1) (lift (1+from) amount t2) ].
67
68 let rec subst (ww : PT) (fw:nat) (w:PT) on w : PT ≝
69   match w with
70   [ Var n ⇒  if eqb n fw then ww else if ltb fw n then Var (pred n) else w fi fi
71   | Lam t ⇒ Lam (subst (lift 1 1 ww) (1+fw) t)
72   | Appl t1 t2 ⇒ Appl (subst ww fw t1) (subst ww fw t2)
73   | Bang t ⇒ Bang (subst ww fw t)
74   | Sect t ⇒ Sect (subst ww fw t) 
75   | LetB t1 t2 ⇒ LetB (subst ww fw t1) (subst (lift 1 1 ww) (1+fw) t2)
76   | LetS t1 t2 ⇒ LetS (subst ww fw t1) (subst (lift 1 1 ww) (1+fw) t2) ]. 
77
78 definition path ≝ list bool.  
79   
80 definition fire ≝ λt:PT.
81   match t with
82   [ Appl hd arg ⇒ 
83       match hd with
84       [ Lam bo ⇒ subst arg 1 bo
85       | _ ⇒ t ]
86   | LetB def bo ⇒ 
87       match def with
88       [ Bang t ⇒ subst t 1 bo
89       | _ ⇒ t ]
90   | LetS def bo ⇒ 
91       match def with
92       [ Sect t ⇒ subst t 1 bo
93       | LetS def2 bo2 ⇒ LetS def2 (LetS bo2 bo)
94       | _ ⇒ t ]
95   | _ ⇒ t ].
96
97 let rec follow (p:path) (t:PT) (f : PT → PT) on p : PT ≝
98   match p with
99   [ nil ⇒ f t
100   | cons b tl ⇒ 
101       match t with
102       [ Var _ ⇒ t
103       | Lam t1 ⇒ if b then t else Lam (follow tl t1 f) fi
104       | Appl t1 t2 ⇒ if b then Appl t1 (follow tl t2 f) else Appl (follow tl t1 f) t2 fi
105       | Bang t1 ⇒ if b then t else Bang (follow tl t1 f) fi
106       | Sect t1 ⇒ if b then t else Sect (follow tl t1 f) fi
107       | LetB t1 t2 ⇒ if b then LetB t1 (follow tl t2 f) else LetB (follow tl t1 f) t2 fi 
108       | LetS t1 t2 ⇒ if b then LetS t1 (follow tl t2 f) else LetS (follow tl t1 f) t2 fi ]].
109
110 definition reduce ≝ λp,t.follow p t fire.
111
112 let rec FO (w:nat) (t:PT) on t : nat ≝ 
113   match t with
114   [ Var n ⇒ if eqb w n then 1 else 0 fi 
115   | Lam t ⇒ FO (1+w) t
116   | Appl t1 t2 ⇒ FO w t1 + FO w t2
117   | Bang t ⇒ FO w t
118   | Sect t ⇒ FO w t
119   | LetB t1 t2 ⇒ FO w t1 + FO (1+w) t2
120   | LetS t1 t2 ⇒ FO w t1 + FO (1+w) t2 ].
121   
122 let rec FOa (w:nat) (t:PT) on t : nat ≝ 
123   match t with
124   [ Var n ⇒ if ltb w n then 1 else 0 fi 
125   | Lam t ⇒ FOa (1+w) t
126   | Appl t1 t2 ⇒ FOa w t1 + FOa w t2
127   | Bang t ⇒ FOa w t
128   | Sect t ⇒ FOa w t
129   | LetB t1 t2 ⇒ FOa w t1 + FOa (1+w) t2
130   | LetS t1 t2 ⇒ FOa w t1 + FOa (1+w) t2 ].
131
132 inductive ctxe : Type ≝ 
133   | Reg: ctxe
134   | Ban: ctxe
135   | Sec: ctxe
136   | Err: ctxe.
137
138 let rec mapb (l : list ctxe) : list ctxe ≝ 
139   match l with
140   [ nil ⇒ nil ?
141   | cons x xs ⇒ 
142       match x with
143       [ Ban ⇒ Reg
144       | _ ⇒ Err ] :: mapb xs].
145
146 let rec maps (l : list ctxe) : list ctxe ≝ 
147   match l with
148   [ nil ⇒ nil ?
149   | cons x xs ⇒ 
150       match x with
151       [ Ban ⇒ Reg
152       | Sec ⇒ Reg
153       | _ ⇒ Err ] :: maps xs].
154
155 inductive Tok : PT → list ctxe → Prop ≝ 
156   | Tv : ∀n,C. nth ? (Err::C) Err n = Reg → Tok (Var n) C
157   | Tl : ∀t,C. Tok t (Reg::C) → FO 1 t ≤ 1 → Tok (Lam t) C
158   | Ta : ∀t1,t2,C. Tok t1 C → Tok t2 C → Tok (Appl t1 t2) C 
159   | Tb : ∀t,C.FOa 0 t ≤ 1 → Tok t (mapb C)  → Tok (Bang t) C
160   | Ts : ∀t,C.Tok t (maps C)  → Tok (Sect t) C
161   | Tlb: ∀t1,t2,C. Tok t1 C → Tok t2 (Ban::C) → Tok (LetB t1 t2) C
162   | Tls: ∀t1,t2,C. Tok t1 C → Tok t2 (Sec::C) → FO 1 t2 ≤ 1 → Tok (LetS t1 t2) C.
163   
164 (* powerup! *)
165 include "decidable_kit/eqtype.ma".  
166   
167 definition cmpC : ctxe → ctxe → bool ≝ 
168   λc1,c2.
169     match c1 with 
170     [ Reg ⇒ match c2 with [ Reg ⇒ true | _ ⇒ false ] 
171     | Ban ⇒ match c2 with [ Ban ⇒ true | _ ⇒ false ]
172     | Sec ⇒ match c2 with [ Sec ⇒ true | _ ⇒ false ]
173     | Err ⇒ match c2 with [ Err ⇒ true | _ ⇒ false ]].
174     
175 lemma cmpCP: ∀x,y.eq_compatible ? x y (cmpC x y).
176 intros; apply prove_reflect; cases x; cases y; simplify; intro;
177 destruct H; try reflexivity; intro W; destruct W;
178 qed.
179
180 definition ctxe_eqType ≝ mk_eqType ?? cmpCP.   
181   
182 let rec Tok_dec (C:list ctxe) (t:PT) on t : bool ≝
183   match t with
184   [ Var n ⇒ cmp ctxe_eqType (nth ? (Err::C) Err n) Reg
185   | Lam t ⇒ andb (Tok_dec (Reg::C) t) (leb (FO 1 t) 1)
186   | Appl t1 t2 ⇒ andb (Tok_dec C t1) (Tok_dec C t2) 
187   | Bang t ⇒ andb (leb (FOa 0 t) 1) (Tok_dec (mapb C) t)
188   | Sect t ⇒ Tok_dec (maps C) t
189   | LetB t1 t2 ⇒ andb (Tok_dec C t1) (Tok_dec (Ban::C) t2)
190   | LetS t1 t2 ⇒ andb (Tok_dec C t1) (andb (Tok_dec (Sec::C) t2) (leb (FO 1 t2) 1))
191   ].
192   
193 (* (constructor ?) tactic *)
194 notation "#" non associative with precedence 90 for @{ 'Tok }.
195 interpretation "Tv" 'Tok = Tv. interpretation "Tl" 'Tok = Tl.
196 interpretation "Ta" 'Tok = Ta. interpretation "Tb" 'Tok = Tb.
197 interpretation "Ts" 'Tok = Ts. interpretation "Tlb" 'Tok = Tlb.
198 interpretation "Tls" 'Tok = Tls.
199   
200 lemma TokP : ∀t,C.reflect (Tok t C) (Tok_dec C t).
201 intros; apply prove_reflect; generalize in match C; elim t; intros;
202 [1,2,3,4,5,6,7: apply rule #; simplify in H H1 H2;
203   [1: apply (b2pT ?? (cmpCP ??) H);
204   |2,7: cases (b2pT ?? (andbP ??) H1); apply (b2pT ?? (lebP ??)); assumption;
205   |3,6: cases (b2pT ?? (andbP ??) H1); autobatch depth=2;
206   |4,5,9,10,13: cases (b2pT ?? (andbP ??) H2); autobatch depth=2;
207   |8: autobatch depth=2;
208   |11: cases (b2pT ?? (andbP ??) H2); cases (b2pT ?? (andbP ??) H4);
209        apply (b2pT ?? (lebP ??)); assumption;
210   |12,11: cases (b2pT ?? (andbP ??) H2); cases (b2pT ?? (andbP ??) H4); autobatch depth=2;]
211 |*: intro E; inversion E; clear E; intros; simplify in H;
212     [1: destruct H3; destruct H2; rewrite > H1 in H; normalize in H; destruct H;
213     |9: destruct H6; destruct H5; simplify in H1;
214         cases (b2pF ?? (andbP ??) H1); split[2:apply (p2bT ?? (lebP ??) H4);] 
215         lapply depth=0 (H (Reg::l)) as W; cases (Tok_dec (Reg::l) p) in W;
216         intros; [reflexivity] cases (H5 ? H2); reflexivity; 
217     |17: destruct H7; destruct H8; simplify in H2; apply (b2pF ?? (andbP ??) H2);
218          lapply depth=0 (H l) as W1; lapply depth=0 (H1 l) as W2; 
219          cases (Tok_dec l p) in W1; cases (Tok_dec l p1) in W2;
220          intros; split; try reflexivity;
221          [1,3: cases (H7 ? H5); reflexivity;|*: cases (H8 ? H3); reflexivity;]
222     |25: destruct H6; destruct H5; simplify in H1;
223          apply (b2pF ?? (andbP ??) H1); rewrite > (p2bT ?? (lebP ??) H2);
224          split[reflexivity] lapply depth=0 (H (mapb l)) as W; 
225          cases (Tok_dec (mapb l) p) in W; intros; [reflexivity] 
226          cases (H5 ? H3); reflexivity;
227     |33: destruct H5; destruct H4; simplify in H1; exact (H ? H1 H2);
228     |41: destruct H8; destruct H6; destruct H7; clear H4 H6; simplify in H2;
229          lapply depth=0 (H l) as W1; lapply depth=0 (H1 (Ban::l)) as W2;
230          apply (b2pF ?? (andbP ??) H2); cases (Tok_dec l p) in W1; 
231          cases (Tok_dec (Ban::l) p1) in W2; intros; split; try reflexivity;
232          [1,3: cases (H4 ? H5); reflexivity;|*: cases (H6 ? H3); reflexivity;]
233     |49: destruct H9; destruct H8; clear H6 H4; simplify in H2;
234          apply (b2pF ?? (andbP ??) H2); clear H2; rewrite > (p2bT ?? (lebP ??) H7);
235          rewrite > andb_sym; simplify; 
236          lapply depth=0 (H l) as W1; lapply depth=0 (H1 (Sec::l)) as W2;
237          cases (Tok_dec l p) in W1; cases (Tok_dec (Sec::l) p1) in W2;
238          intros; split; try reflexivity;
239          [1,3: cases (H2 ? H5); reflexivity;|*: cases (H4 ? H3); reflexivity;]
240     |*: try solve[destruct H3]; try solve[destruct H4]; try solve[destruct H5];
241         try solve[destruct H6]; try solve[destruct H7]; try solve[destruct H8]]]
242 qed.
243
244 definition two : PT ≝ *Λ(§Λ𝟚(𝟚𝟙)).
245 definition succ : PT ≝ Λ*Λ(LetS (𝟛 (!𝟙)) §(Λ𝟛 (𝟚 𝟙))).
246 definition three : PT ≝ *Λ(§Λ𝟚(𝟚(𝟚 𝟙))).
247
248 lemma two_Tok : Tok two [ ]. apply (b2pT ?? (TokP ??)); reflexivity; qed.
249 lemma succ_Tok : Tok succ [ ]. apply (b2pT ?? (TokP ??)); reflexivity; qed.
250 lemma three_Tok : Tok three [ ]. apply (b2pT ?? (TokP ??)); reflexivity; qed.
251
252 definition foldl ≝ 
253   λA,B:Type.λf:A → B → B.
254   let rec aux (acc: B) (l:list A) on l  ≝ 
255     match l with
256     [ nil ⇒  acc
257     | cons x xs ⇒ aux (f x acc) xs]
258   in 
259     aux.
260
261 lemma obvious : ∃pl.foldl ?? reduce (succ two) pl = three.
262 unfold succ; unfold two; exists; 
263 [apply ([ ] :: ?);| simplify;]
264 [apply ([false;true;false] :: ?);| simplify;]
265 [apply ([false;true;false] :: ?);| simplify;]
266 [apply ([false;true] :: ?);| simplify;]
267 [apply ([false;true;false;false;true] :: ?);| simplify;]
268 [apply ([ ]);| simplify;]
269 reflexivity;
270 qed.