diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Bool/Bool.v | 4 | ||||
| -rw-r--r-- | theories/Zarith/Wf_Z.v | 2 | ||||
| -rw-r--r-- | theories/Zarith/Zmisc.v | 32 | ||||
| -rw-r--r-- | theories/Zarith/Zsyntax.v | 8 |
4 files changed, 36 insertions, 10 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 7f8f52c4f6..ab1a4b9e04 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -106,6 +106,7 @@ Lemma Is_true_eq_true2 : (x:bool) x=true -> (Is_true x). Destruct x; Simpl; Auto with bool. Save. +(***** TODO Lemma eqb_subst : (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2). Unfold eqb . @@ -121,7 +122,8 @@ Intros H. Inversion_clear H. Trivial with bool. Save. - +*****) + Lemma eqb_reflx : (b:bool)(eqb b b)=true. Intro b. Case b. diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v index 389db702ca..6b015c77f4 100644 --- a/theories/Zarith/Wf_Z.v +++ b/theories/Zarith/Wf_Z.v @@ -25,7 +25,7 @@ Require Zsyntax. Then the diagram will be closed and the theorem proved. *) Lemma inject_nat_complete : - (x:Z)`0 <= x` -> (Ex [n:nat](x=(inject_nat n))). + (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)). Destruct x; Intros; [ Exists O; Auto with arith | Specialize (ZL4 p); Intros Hp; Elim Hp; Intros; diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v index 888d2fb81a..28c4cf2084 100644 --- a/theories/Zarith/Zmisc.v +++ b/theories/Zarith/Zmisc.v @@ -207,28 +207,52 @@ Definition Zodd_bool := Lemma Zeven_odd_dec : (z:Z) { (Zeven z) }+{ (Zodd z) }. Proof. + Intro z. Case z; + [ Left; Compute; Trivial + | Intro p; Case p; Intros; + (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) + | Intro p; Case p; Intros; + (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ]. + (*** was Realizer Zeven_bool. Repeat Program; Compute; Trivial. + ***) Save. Lemma Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }. Proof. + Intro z. Case z; + [ Left; Compute; Trivial + | Intro p; Case p; Intros; + (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) + | Intro p; Case p; Intros; + (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. + (*** was Realizer Zeven_bool. Repeat Program; Compute; Trivial. + ***) Save. Lemma Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }. Proof. + Intro z. Case z; + [ Right; Compute; Trivial + | Intro p; Case p; Intros; + (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) + | Intro p; Case p; Intros; + (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. + (*** was Realizer Zodd_bool. Repeat Program; Compute; Trivial. + ***) Save. -Lemma Zeven_not_Zodd : (z:Z)(Zeven z)->~(Zodd z). +Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z). Proof. Destruct z; [ Idtac | Destruct p | Destruct p ]; Compute; Trivial. Save. -Lemma Zodd_not_Zeven : (z:Z)(Zodd z)->~(Zeven z). +Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z). Proof. Destruct z; [ Idtac | Destruct p | Destruct p ]; Compute; Trivial. Save. @@ -320,7 +344,7 @@ Apply rename with x:=`x ?= y`; Intro r; Elim r; Save. Lemma Zcompare_x_x : (x:Z) `x ?= x` = EGAL. -(Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2:?]h2 end). +(Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2: ?]h2 end). Apply refl_equal. Save. @@ -339,7 +363,7 @@ Save. Lemma Zcompare_eq_case : (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y -> (Case `x ?= y` of c1 c2 c3 end). Intros. -Rewrite -> (Case (Zcompare_EGAL x y) of [h1,h2:?]h2 end H0). +Rewrite -> (Case (Zcompare_EGAL x y) of [h1,h2: ?]h2 end H0). Assumption. Save. diff --git a/theories/Zarith/Zsyntax.v b/theories/Zarith/Zsyntax.v index 0fb1e6b72f..350bcaa180 100644 --- a/theories/Zarith/Zsyntax.v +++ b/theories/Zarith/Zsyntax.v @@ -34,8 +34,8 @@ with formula := -> [<<(Zlt $p $c)/\(Zle $c $c1)>>] | form_lt_lt [ expr($p) "<" expr($c) "<" expr($c1) ] -> [<<(Zlt $p $c)/\(Zlt $c $c1)>>] -| form_neq [ expr($p) "<>" expr($c) ] -> [<<~(eq Z $p $c)>>] -| form_comp [ expr($p) "?" "=" expr($c) ] -> [<<(Zcompare $p $c)>>] +| form_neq [ expr($p) "<>" expr($c) ] -> [<< ~(eq Z $p $c)>>] +| form_comp [ expr($p) "?=" expr($c) ] -> [<<(Zcompare $p $c)>>] with expr := expr_plus [ expr($p) "+" expr($c) ] -> [<<(Zplus $p $c)>>] @@ -60,7 +60,7 @@ with expr0 := with application := apply [ application($p) expr($c1) ] -> [<<($p $c1)>>] -| pair [ expr($p) "," expr($c) ] -> [<<($p,$c)>>] +| pair [ expr($p) "," expr($c) ] -> [<<($p, $c)>>] | appl0 [ expr($a) ] -> [$a] . @@ -99,7 +99,7 @@ Syntax constr [[<hov 0> "`" (ZEXPR $n1) [1 0] "?= " (ZEXPR $n2) "`" ]] | Zeq [<<(eq Z $n1 $n2)>>] -> [[<hov 0> "`" (ZEXPR $n1) [1 0] "= "(ZEXPR $n2)"`"]] - | Zneq [<<~(eq Z $n1 $n2)>>] -> + | Zneq [<< ~(eq Z $n1 $n2)>>] -> [[<hov 0> "`" (ZEXPR $n1) [1 0] "<> "(ZEXPR $n2) "`"]] | Zle_Zle [<<(Zle $n1 $n2)/\(Zle $n2 $n3)>>] -> [[<hov 0> "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2) |