Changeset 2520
 Timestamp:
 Dec 3, 2012, 4:07:45 PM (7 years ago)
 Location:
 Papers/polymorphicvariants2012
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/test.ma
r2514 r2520 26 26  Mul _ _ => mul ]. 27 27 28 (*29 28 definition Q_holds_for_tag: 30 ∀E:Type[0]. ∀ l: list tag. ∀Q: ∀x: l E → Prop. ∀t:tag. memb … t l →Prop ≝31 λE, l,Q,t. ?.32 match t return λt. memb … t l → Propwith33 [ num ⇒ λH. (∀n. Q (Num … n))34  plus ⇒ λH. (∀x,y. Q (Plus … x y))35  mul ⇒ λH. (∀x,y. Q (Mul … x y))29 ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop ≝ 30 λE,Q,t. 31 match t with 32 [ num ⇒ ∀n. Q (Num … n) 33  plus ⇒ ∀x,y. Q (Plus … x y) 34  mul ⇒ ∀x,y. Q (Mul … x y) 36 35 ]. 37 36 38 39 definition Q_holds_for_tag: 40 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝ 41 λE,l,Q,t. ?. 42 match t return λt. memb … t l → Prop with 43 [ num ⇒ λH. (∀n. Q (Num … n)) 44  plus ⇒ λH. (∀x,y. Q (Plus … x y)) 45  mul ⇒ λH. (∀x,y. Q (Mul … x y)) 46 ]. 47 48 axiom Q_holds_for_tag_spec: 49 ∀E:Type[0]. ∀fixed_l: list tag. ∀Q: fixed_l E → Prop. ∀t:tag. 50 ∀p:memb … t fixed_l. Q_holds_for_tag … Q … p → 51 ∀x: [t] E. Q x. 52 *) 37 theorem Q_holds_for_tag_spec: 38 ∀E:Type[0]. ∀Q: expr E → Prop. 39 ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x. 40 #E #Q * normalize // 41 qed. 
Papers/polymorphicvariants2012/variants.ma
r2514 r2520 1 (*include "infrastructure.ma".*)2 include "test.ma".3 4 1 (* 2 include "infrastructure.ma". 5 3 axiom tag: DeqSet. 6 4 axiom expr: Type[0] → Type[0]. 7 5 axiom tag_of_expr: ∀E:Type[0]. expr E → tag. 6 axiom Q_holds_for_tag: ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop. 7 axiom Q_holds_for_tag_spec: 8 ∀E:Type[0]. ∀Q: expr E → Prop. 9 ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x. 8 10 *) 11 12 include "test.ma". 9 13 10 14 definition is_in : ∀E: Type[0]. list tag > expr E > bool ≝ … … 25 29 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?. 26 30 27 (* 28 axiom Q_holds_for_tag: 29 ∀E:Type[0]. ∀fixed_l: list tag. ∀Q: fixed_l E → Prop. ∀t:tag. 30 memb … t fixed_l → Prop.*) 31 definition Q_of_Q': 32 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. expr E → Prop ≝ 33 λE,l,Q,e. 34 match memb … (tag_of_expr … e) l return λx. memb … (tag_of_expr … e) l = x → Prop with 35 [ true ⇒ λH. Q e 36  false ⇒ λH. False 37 ] (refl …). 38 whd in match (is_in ???); >H // 39 qed. 31 40 32 definition Q_holds_for_tag: 41 lemma dep_bool_match_elim : 42 ∀b.∀B : Type[0].∀P : B → Prop.∀Q : bool → Prop. 43 ∀c1,c2. 44 (∀prf : Q true.P (c1 prf)) → 45 (∀prf : Q false.P (c2 prf)) → 46 ∀prf : Q b. 47 P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf  false ⇒ λprf.c2 prf ] prf). 48 * // qed. 49 50 lemma Q_of_Q_ok': 51 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀x:l E. 52 Q_of_Q' E l Q x→Q x. 53 #E #l #Q #x normalize 54 @(dep_bool_match_elim (tag_of_expr E x ∈ l)) [2: #_ *] 55 cases x #y #prf' #prf'' #H @H 56 qed. 57 58 definition Q_holds_for_tag': 33 59 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝ 34 λE,l,Q,t. 35 match t return λt. memb … t l → Prop with 36 [ num ⇒ λH. (∀n. Q (Num … n)) 37  plus ⇒ λH. (∀x,y. Q (Plus … x y)) 38  mul ⇒ λH. (∀x,y. Q (Mul … x y)) 39 ]. 40 // qed. 60 λE,l,Q',t,p. 61 Q_holds_for_tag E (Q_of_Q' … l Q') t. 41 62 42 (* 43 axiom Q_holds_for_tag_spec: 44 ∀E:Type[0]. ∀fixed_l: list tag. ∀Q: fixed_l E → Prop. ∀t:tag. 45 ∀p:memb … t fixed_l. Q_holds_for_tag … Q … p → 46 ∀x: [t] E. Q x. 47 cases x #y #H @(memb_to_sublist_to_memb … H) whd in match (sublist ???); 48 cases (memb ???) in p; // 49 qed. 50 *) 51 52 theorem Q_holds_for_tag_spec: 63 theorem Q_holds_for_tag_spec': 53 64 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. 54 ∀p:memb … t l. Q_holds_for_tag … Q … p →65 ∀p:memb … t l. Q_holds_for_tag' … Q … p → 55 66 ∀x: [t] E. Q x. 56 67 [2: cases x #y #H @(memb_to_sublist_to_memb … H) whd in match (sublist ???); 57 68 cases (memb ???) in p; // 58  #E #l #Q * normalize #H #K ** // try (#x #y #IN) try (#x #IN) try #IN 59 cases IN ] 69  #E #l #Q #t #p whd in match Q_holds_for_tag'; normalize nodelta #H #x 70 cut (t = tag_of_expr … x) 71 [ cases x x #x #EQ whd in EQ; inversion (is_in E [t] x) in EQ; 72 normalize nodelta 73 [2: #_ #abs cases abs] whd in ⊢ (??%? → ? → ?); 74 inversion (tag_of_expr E x == t) [2: #_ normalize #abs destruct] 75 #EQ #_ #_ <(\P EQ) % 76  #EQ2 lapply H >EQ2 in ⊢ (% → ?); #K lapply(Q_holds_for_tag_spec … K) 77 cut (tag_of_expr E x ∈ l) // #K1 #K2 @(Q_of_Q_ok' E l Q x) 78 cases x in K2; // ]] 60 79 qed. 61 80 … … 69 88  cons hd tl ⇒ λH. 70 89 let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in 71 Q_holds_for_tag … fixed_l Q hd (sublist_hd_tl_to_memb … hd tl fixed_l H) →90 Q_holds_for_tag' … fixed_l Q hd (sublist_hd_tl_to_memb … hd tl fixed_l H) → 72 91 tail_call ]. 73 92 /2/ qed. … … 81 100 #hd #tl #IH (*cases hd*) #H #INV whd #P0 @IH #y 82 101 whd in match (is_in ???) in INV:%; 83 lapply (Q_holds_for_tag_spec … P0) #K1 #K2102 lapply (Q_holds_for_tag_spec' … P0) #K1 #K2 84 103 inversion (tag_of_expr … y == hd) #K3 85 104 [ lapply (K1 y)
Note: See TracChangeset
for help on using the changeset viewer.