Changeset 985 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (8 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r907 r985  
    361361 /3/
    362362qed.
     363
     364lemma inclusive_disjunction_true:
     365  ∀b, c: bool.
     366    (orb b c) = true → b = true ∨ c = true.
     367  # b
     368  # c
     369  elim b
     370  [ normalize
     371    # H
     372    @ or_introl
     373    %
     374  | normalize
     375    /2/
     376  ]
     377qed.
     378
     379lemma conjunction_true:
     380  ∀b, c: bool.
     381    andb b c = true → b = true ∧ c = true.
     382  # b
     383  # c
     384  elim b
     385  normalize
     386  [ /2/
     387  | # K
     388    destruct
     389  ]
     390qed.
     391
     392lemma eq_true_false: false=true → False.
     393 # K
     394 destruct
     395qed.
     396
     397lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
     398 # b
     399 cases b
     400 %
     401qed.
     402
     403definition bool_to_Prop ≝
     404 λb. match b with [ true ⇒ True | false ⇒ False ].
     405
     406coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     407
     408lemma eq_false_to_notb: ∀b. b = false → ¬ b.
     409 *; /2/
     410qed.
     411
     412lemma length_append:
     413 ∀A.∀l1,l2:list A.
     414  |l1 @ l2| = |l1| + |l2|.
     415 #A #l1 elim l1
     416  [ //
     417  | #hd #tl #IH #l2 normalize <IH //]
     418qed.
Note: See TracChangeset for help on using the changeset viewer.