Commit 501bde2a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update some Coq realizations.

parent b2ca71c0
......@@ -102,9 +102,10 @@ apply natlike_ind.
now rewrite Zmult_0_r, 2!Power_0.
intros m Hm IHm.
replace (n * Zsucc m)%Z with (n * m + n)%Z by ring.
rewrite Power_sum by auto with zarith.
unfold Zsucc.
rewrite 2!Power_sum by auto with zarith.
rewrite IHm.
now rewrite Comm, <- Power_s.
now rewrite Power_1.
Qed.
(* Why3 goal *)
......
......@@ -16,20 +16,7 @@ Require BuiltIn.
Require HighOrd.
Require map.Map.
(* Why3 goal *)
Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (a -> b).
Proof.
intros a a_WT b b_WT v.
intros i.
exact v.
Defined.
(* Why3 goal *)
Lemma const_def : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (v:b), forall (us:a), (((const v: (a -> b)) us) = v).
Proof.
intros a a_WT b b_WT b1 a1.
reflexivity.
Qed.
(* Why3 assumption *)
Definition const {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}
(v:b): (a -> b) := fun (us:a) => v.
......@@ -15,11 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require Import ClassicalEpsilon.
(* Why3 assumption *)
......@@ -47,7 +42,7 @@ Defined.
(* Why3 goal *)
Lemma set_def : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (f:(a -> b)) (x:a) (v:b), forall (y:a), ((y = x) -> (((set f x v)
forall (f:(a -> b)) (x:a) (v:b) (y:a), ((y = x) -> (((set f x v)
y) = v)) /\ ((~ (y = x)) -> (((set f x v) y) = (f y))).
Proof.
intros a a_WT b b_WT f x v y.
......
......@@ -157,13 +157,21 @@ intros a a_WT s1 s2.
exact (fun x => orb (s1 x) (s2 x)).
Defined.
(* Why3 goal *)
Lemma union_def : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
(s2:(a -> bool)) (x:a), (((union s1 s2) x) = true) <-> (((s1 x) = true) \/
((s2 x) = true)).
Proof.
intros a a_WT s1 s2 x.
apply Bool.orb_true_iff.
Qed.
(* Why3 goal *)
Lemma union_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
(s2:(a -> bool)), forall (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/
(mem x s2)).
Proof.
intros a a_WT s1 s2 x.
apply Bool.orb_true_iff.
exact @union_def.
Qed.
(* Why3 goal *)
......@@ -174,13 +182,21 @@ intros a a_WT s1 s2.
exact (fun x => andb (s1 x) (s2 x)).
Defined.
(* Why3 goal *)
Lemma inter_def : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
(s2:(a -> bool)) (x:a), (((inter s1 s2) x) = true) <-> (((s1 x) = true) /\
((s2 x) = true)).
Proof.
intros a a_WT s1 s2 x.
apply Bool.andb_true_iff.
Qed.
(* Why3 goal *)
Lemma inter_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
(s2:(a -> bool)), forall (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\
(mem x s2)).
Proof.
intros a a_WT s1 s2 x.
apply Bool.andb_true_iff.
exact @inter_def.
Qed.
(* Why3 goal *)
......@@ -192,9 +208,9 @@ exact (fun x => andb (s1 x) (negb (s2 x))).
Defined.
(* Why3 goal *)
Lemma diff_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
(s2:(a -> bool)), forall (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\
~ (mem x s2)).
Lemma diff_def : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
(s2:(a -> bool)) (x:a), (((diff s1 s2) x) = true) <-> (((s1 x) = true) /\
~ ((s2 x) = true)).
Proof.
intros a a_WT s1 s2 x.
unfold mem, diff.
......@@ -203,6 +219,14 @@ rewrite <- Bool.negb_true_iff.
apply Bool.andb_true_iff.
Qed.
(* Why3 goal *)
Lemma diff_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
(s2:(a -> bool)), forall (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\
~ (mem x s2)).
Proof.
exact @diff_def.
Qed.
(* Why3 goal *)
Lemma subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
(s2:(a -> bool)), (subset (diff s1 s2) s1).
......@@ -222,7 +246,7 @@ Defined.
(* Why3 goal *)
Lemma complement_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(a ->
bool)), forall (x:a), (((complement s) x) = true) <-> ~ ((s x) = true).
bool)) (x:a), (((complement s) x) = true) <-> ~ ((s x) = true).
Proof.
intros a a_WT s x.
unfold complement.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment