source: src/utilities/extralib.ma @ 1523

Last change on this file since 1523 was 1523, checked in by campbell, 9 years ago

Separate out positive and Z definitions from extralib.ma.
Minor syntax updates.

File size: 2.6 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "basics/types.ma".
16include "basics/list.ma".
17include "basics/logic.ma".
18include "utilities/pair.ma".
19
20lemma eq_rect_Type0_r:
21 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
22 #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption.
23qed.
24
25lemma eq_rect_r2:
26 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
27 #A #a #x #p cases p; #P #H assumption.
28qed.
29
30lemma eq_rect_Type2_r:
31 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
32 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption.
33qed.
34
35lemma eq_rect_CProp0_r:
36 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
37 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption.
38qed.
39
40lemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
41#A #x #y *;#H @nmk #H' /2/;
42qed.
43
44interpretation "logical iff" 'iff x y = (iff x y).
45
46(* bool *)
47
48definition xorb : bool → bool → bool ≝
49  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
50 
51 
52 
53
54(* should be proved in nat.ma, but it's not! *)
55lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
56#n elim n;
57[ #m cases m; //;
58| #n' #IH #m cases m; [ /2/; | #m' whd in match (eqb (S n') (S m')) in ⊢ %;
59  lapply (IH m'); cases (eqb n' m'); /2/; ]
60] qed.
61
62(* datatypes/list.ma *)
63
64theorem nil_append_nil_both:
65  ∀A:Type[0]. ∀l1,l2:list A.
66    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
67#A #l1 #l2 cases l1
68[ cases l2
69  [ /2/
70  | normalize #h #t #H destruct
71  ]
72| cases l2
73  [ normalize #h #t #H destruct
74  | normalize #h1 #t1 #h2 #h3 #H destruct
75  ]
76] qed.
Note: See TracBrowser for help on using the repository browser.