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

Now it is nice!

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.