Changeset 1882 for src/ASM/Util.ma


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1811 r1882  
    1212notation "⊥" with precedence 90
    1313  for @{ match ? in False with [ ] }.
     14notation "Ⓧ" with precedence 90
     15  for @{ λabs.match abs in False with [ ] }.
     16
    1417
    1518definition ltb ≝
     
    561564    foldr ? ? (append ?) [ ] l.
    562565
    563 let rec rev (A: Type[0]) (l: list A) on l ≝
    564   match l with
    565   [ nil ⇒ nil A
    566   | cons hd tl ⇒ (rev A tl) @ [ hd ]
    567   ].
     566(* redirecting to library reverse *)
     567definition rev ≝ reverse.
    568568
    569569lemma append_length:
     
    594594  elim L
    595595  [ normalize >append_nil %
    596   | #HD #TL #IH
    597     normalize >IH
     596  | #HD #TL normalize #IH
     597    >rev_append_def
     598    >rev_append_def
     599    >rev_append_def
     600    >append_nil
     601    normalize
     602    >IH
    598603    @associative_append
    599604  ]
     
    607612  elim L
    608613  [ %
    609   | #HD #TL #IH
    610     normalize
     614  | #HD #TL normalize #IH
     615    >rev_append_def
    611616    >(append_length A (rev A TL) [HD])
    612     normalize /2/
     617    normalize /2 by /
    613618  ]
    614619qed.
     
    834839coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    835840
     841lemma bool_as_Prop_to_eq : ∀b : bool. b → b = true.
     842**%
     843qed.
     844
     845(* with this you can use prf : b with b : bool with rewriting
     846   >prf rewrites b as true *)
     847coercion bool_to_Prop_to_eq : ∀b : bool.∀prf : b.b = true
     848 ≝ bool_as_Prop_to_eq on _prf : bool_to_Prop ? to (? = true).
     849
     850lemma andb_Prop : ∀b,d : bool.b → d → b∧d.
     851#b #d #btrue #dtrue >btrue >dtrue %
     852qed.
     853
     854lemma andb_Prop_true : ∀b,d : bool. (b∧d) → And (bool_to_Prop b) (bool_to_Prop d).
     855#b #d #bdtrue elim (andb_true … bdtrue) #btrue #dtrue >btrue >dtrue % %
     856qed.
     857
     858lemma orb_Prop_l : ∀b,d : bool.b → b∨d.
     859#b #d #btrue >btrue %
     860qed.
     861
     862lemma orb_Prop_r : ∀b,d : bool.d → b∨d.
     863#b #d #dtrue >dtrue elim b %
     864qed.
     865
     866lemma orb_Prop_true : ∀b,d : bool. (b∨d) → Or (bool_to_Prop b) (bool_to_Prop d).
     867#b #d #bdtrue elim (orb_true_l … bdtrue) #xtrue >xtrue [%1 | %2] %
     868qed.
     869
     870lemma notb_Prop : ∀b : bool. Not (bool_to_Prop b) → notb b.
     871* * #H [@H % | %]
     872qed.
     873
    836874lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    837  *; /2/
    838 qed.
     875 *; /2 by eq_true_false, I/
     876qed.
     877
     878lemma not_b_to_eq_false : ∀b : bool. Not (bool_to_Prop b) → b = false.
     879** #H [elim (H ?) % | %]
     880qed.
     881
     882(* with this you can use prf : ¬b with b : bool with rewriting
     883   >prf rewrites b as false *)
     884coercion not_bool_to_Prop_to_eq : ∀b : bool.∀prf : Not (bool_to_Prop b).b = false
     885 ≝ not_b_to_eq_false on _prf : Not (bool_to_Prop ?) to (? = false).
     886
     887
     888lemma true_or_false_Prop : ∀b : bool.Or (bool_to_Prop b) (¬(bool_to_Prop b)).
     889* [%1 % | %2 % *]
     890qed.
     891
     892lemma eq_true_to_b : ∀b. b = true → b.
     893#b #btrue >btrue %
     894qed.
     895
     896definition if_then_else_safe : ∀A : Type[0].∀b : bool.(b → A) → (¬(bool_to_Prop b) → A) → A ≝
     897  λA,b,f,g.
     898  match b return λx.match x with [true ⇒ bool_to_Prop b | false ⇒ ¬bool_to_Prop b] → A with
     899  [ true ⇒ f
     900  | false ⇒ g
     901  ] ?. elim b % *
     902qed.
     903
     904notation > "'If' b 'then' 'with' ident prf1 'do' f 'else' 'with' ident prf2 'do' g" with precedence 46 for
     905  @{'if_then_else_safe $b (λ${ident prf1}.$f) (λ${ident prf2}.$g)}.
     906notation > "'If' b 'then' 'with' ident prf1 : ty1 'do' f 'else' 'with' ident prf2 : ty2 'do' g" with precedence 46 for
     907  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     908notation > "'If' b 'then' f 'else' 'with' ident prf2 'do' g" with precedence 46 for
     909  @{'if_then_else_safe $b (λ_.$f) (λ${ident prf2}.$g)}.
     910notation > "'If' b 'then' f 'else' 'with' ident prf2 : ty2 'do' g" with precedence 46 for
     911  @{'if_then_else_safe $b (λ_.$f) (λ${ident prf2}:$ty2.$g)}.
     912notation > "'If' b 'then' 'with' ident prf1 'do' f 'else' g" with precedence 46 for
     913  @{'if_then_else_safe $b (λ${ident prf1}.$f) (λ_.$g)}.
     914notation > "'If' b 'then' 'with' ident prf1 : ty1 'do' f 'else' g" with precedence 46 for
     915  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ_.$g)}.
     916
     917notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break 'with' \nbsp ident prf1 : ty1 \nbsp 'do' \nbsp break f \nbsp break 'else' \nbsp break 'with' \nbsp ident prf2 : ty2 \nbsp 'do' \nbsp break g)" with precedence 46 for
     918  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     919notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break f \nbsp break 'else' \nbsp break 'with' \nbsp ident prf2 : ty2 \nbsp 'do' \nbsp break g)" with precedence 46 for
     920  @{'if_then_else_safe $b (λ_:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     921notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break 'with' \nbsp ident prf1 : ty1 \nbsp 'do' \nbsp break f \nbsp break 'else' \nbsp break g)" with precedence 46 for
     922  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ_:$ty2.$g)}.
     923 
     924interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g).
    839925
    840926lemma length_append:
Note: See TracChangeset for help on using the changeset viewer.