Ignore:
Timestamp:
Dec 2, 2012, 4:40:41 PM (7 years ago)
Author:
sacerdot
Message:

All .ma files committed: some of them are just in-progress.

File:
1 edited

Legend:

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

    r2411 r2514  
    1 include "basics/lists/listb.ma".
    2 
    3 definition bool_to_Prop : bool → Prop ≝
    4  λb. match b with [ true ⇒ True | false ⇒ False ].
    5 
    6 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     1include "infrastructure.ma".
    72
    83inductive tag : Type[0] := a : tag | b : tag | c : tag.
     
    3025definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?.
    3126 ** normalize /2/ % #abs destruct
    32 qed.
    33 
    34 definition defined : ∀T:Type[0]. option T → bool ≝
    35  λT,x. match x with [ None ⇒ false | Some _ ⇒ true ].
    36 
    37 let rec for_each (T:Type[0]) (f: T → bool) (l: list T) on l : bool ≝
    38  match l with
    39  [ nil ⇒ true
    40  | cons hd tl ⇒ for_each T f tl ∧ f hd ].
    41 
    42 lemma for_each_to_memb_to_true:
    43  ∀T:DeqSet. ∀f: T → bool. ∀t:T. ∀l: list T.
    44   memb T t l → for_each T f l = true → f t = true.
    45  #T #f #t #l elim l
    46  [ #abs cases abs
    47  | #hd #tl #IH normalize in ⊢ (% → ?); inversion (t == hd) #H normalize
    48    [ #_ cases (for_each ???) normalize
    49      [ <(\P H) // | #abs destruct ]
    50    | cases (t ∈ tl) in IH; normalize
    51      [2: #_ #abs cases abs
    52      | cases (for_each ???) normalize /2/]]
    5327qed.
    5428
Note: See TracChangeset for help on using the changeset viewer.