Changeset 2123 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 27, 2012, 4:04:14 PM (8 years ago)
Author:
boender
Message:
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2111 r2123  
    14941494coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝
    14951495  not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?.
     1496 
     1497lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
     1498  #a #b / by refl/
     1499qed.
     1500
     1501lemma nth_last: ∀A,a,l.
     1502  nth (|l|) A l a = a.
     1503 #A #a #l elim l
     1504 [ / by /
     1505 | #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind
     1506 ]
     1507qed.
     1508
     1509
     1510lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m.
     1511 #n
     1512 elim n
     1513 [ #m #_ @le_O_n
     1514 | #n' #Hind #m cases m
     1515   [ #H -n whd in match (minus ??) in H; >H @le_n
     1516   | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H
     1517   ]
     1518 ]
     1519qed.
     1520
     1521lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.
     1522 #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r
     1523qed.
     1524
     1525(* this can probably be done more simply somewhere *)
     1526lemma not_true_is_false:
     1527  ∀b:bool.b ≠ true → b = false.
     1528 #b cases b
     1529 [ #H @⊥ @(absurd ?? H) @refl
     1530 | #H @refl
     1531 ]
     1532qed.
Note: See TracChangeset for help on using the changeset viewer.