helm/software/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 60 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.