Changeset 2520


Ignore:
Timestamp:
Dec 3, 2012, 4:07:45 PM (7 years ago)
Author:
sacerdot
Message:

Now it is nice!

Location:
Papers/polymorphic-variants-2012
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/test.ma

    r2514 r2520  
    2626   | Mul _ _ => mul ].
    2727
    28 (*
    2928definition 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 → Prop with
    33     [ 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)
    3635    ].
    3736
    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 *)
     37theorem 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 //
     41qed.
  • Papers/polymorphic-variants-2012/variants.ma

    r2514 r2520  
    1 (*include "infrastructure.ma".*)
    2 include "test.ma".
    3 
    41(*
     2include "infrastructure.ma".
    53axiom tag: DeqSet.
    64axiom expr: Type[0] → Type[0].
    75axiom tag_of_expr: ∀E:Type[0]. expr E → tag.
     6axiom Q_holds_for_tag: ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop.
     7axiom 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.
    810*)
     11
     12include "test.ma".
    913
    1014definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
     
    2529 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?.
    2630
    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.*)
     31definition 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 …).
     38whd in match (is_in ???); >H //
     39qed.
    3140
    32 definition Q_holds_for_tag:
     41lemma 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.
     47P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf | false ⇒ λprf.c2 prf ] prf).
     48* // qed.
     49
     50lemma 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
     56qed.
     57 
     58definition Q_holds_for_tag':
    3359 ∀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.
    4162
    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:
     63theorem Q_holds_for_tag_spec':
    5364 ∀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 →
    5566   ∀x: [t] E. Q x.
    5667[2: cases x #y #H @(memb_to_sublist_to_memb … H) whd in match (sublist ???);
    5768    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; // ]]
    6079qed.
    6180
     
    6988 | cons hd tl ⇒ λH.
    7089    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) →
    7291      tail_call ].
    7392/2/ qed.
     
    81100 #hd #tl #IH (*cases hd*) #H #INV whd #P0 @IH #y
    82101 whd in match (is_in ???) in INV:%;
    83  lapply (Q_holds_for_tag_spec … P0) #K1 #K2
     102 lapply (Q_holds_for_tag_spec' … P0) #K1 #K2
    84103 inversion (tag_of_expr … y == hd) #K3
    85104 [ lapply (K1 y)
Note: See TracChangeset for help on using the changeset viewer.