Commit 0e28a82a authored by MARCHE Claude's avatar MARCHE Claude

A Coq realization of set.Set

parent 24586c78
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require Import ClassicalEpsilon.
Require Import FunctionalExtensionality.
(* "it is folklore that the two are consistent" *)
Parameter eq : forall {a:Type} {a_WT:WhyType a}, a -> a -> bool.
Axiom eq_dec:
forall {a:Type} {a_WT:WhyType a} (x y:a),
if eq x y then x=y else x<>y.
(* Why3 goal *)
Definition set : forall (a:Type) {a_WT:WhyType a}, Type.
intros.
exact (a -> bool).
Defined.
(* Why3 goal *)
Definition mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
intros a a_WT x s.
exact (s x = true).
Defined.
Hint Unfold mem.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
(* Why3 goal *)
Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
intros a a_WT s1 s2 h1.
extensionality x.
red in h1.
unfold mem in h1.
generalize (h1 x); clear h1.
intro H.
destruct (s1 x); destruct (s2 x); intuition.
Qed.
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) -> (mem x s2).
(* Why3 goal *)
Lemma subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
s3)).
intros a a_WT s1 s2 s3 h1 h2.
unfold subset; intuition.
Qed.
(* Why3 goal *)
Definition empty: forall {a:Type} {a_WT:WhyType a}, (set a).
intros.
exact (fun _ => false).
Defined.
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
(* Why3 goal *)
Lemma empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set
a))).
intros a a_WT.
unfold is_empty; intuition.
Qed.
(* Why3 goal *)
Definition add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
intros a a_WT x s.
exact (fun y => orb (eq x y) (s y)).
Defined.
(* Why3 goal *)
Lemma add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
intros a a_WT x y s.
unfold add, mem.
generalize (eq_dec y x); intro.
rewrite Bool.orb_true_iff.
destruct (eq y x); intuition.
Qed.
(* Why3 goal *)
Definition remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
intros a a_WT x s.
exact (fun y => andb (negb (eq x y)) (s y)).
Defined.
(* Why3 goal *)
Lemma remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
intros a a_WT x y s.
unfold mem, remove.
generalize (eq_dec y x); intro.
rewrite Bool.andb_true_iff.
destruct (eq y x); intuition.
Qed.
(* Why3 goal *)
Lemma subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (subset (remove x s) s).
intros a a_WT x s.
unfold subset; intro y.
rewrite remove_def1; tauto.
Qed.
(* Why3 goal *)
Definition union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) ->
(set a).
intros a a_WT s1 s2.
exact (fun x => orb (s1 x) (s2 x)).
Defined.
(* Why3 goal *)
Lemma union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
intros a a_WT s1 s2 x.
unfold union, mem.
apply Bool.orb_true_iff.
Qed.
(* Why3 goal *)
Definition inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) ->
(set a).
intros a a_WT s1 s2.
exact (fun x => andb (s1 x) (s2 x)).
Defined.
(* Why3 goal *)
Lemma inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
intros a a_WT s1 s2 x.
unfold inter, mem.
apply Bool.andb_true_iff.
Qed.
(* Why3 goal *)
Definition diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
intros a a_WT s1 s2.
exact (fun x => andb (s1 x) (negb (s2 x))).
Defined.
(* Why3 goal *)
Lemma diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
intros a a_WT s1 s2 x.
unfold diff, mem.
rewrite Bool.andb_true_iff.
rewrite Bool.negb_true_iff.
intuition.
rewrite H in H1; discriminate.
apply Bool.not_true_is_false.
auto.
Qed.
(* Why3 goal *)
Lemma subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset (diff s1 s2) s1).
intros a a_WT s1 s2.
unfold subset; intro x.
rewrite diff_def1; tauto.
Qed.
(* Why3 goal *)
Definition choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
intros a a_WT s.
assert (i: inhabited a) by (apply inhabits; assumption).
exact (epsilon i (fun x => mem x s)).
Defined.
(* Why3 goal *)
Lemma choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(~ (is_empty s)) -> (mem (choose s) s).
intros a a_WT s h.
unfold choose.
apply epsilon_spec.
now apply not_all_not_ex.
Qed.
(* Why3 goal *)
Definition all: forall {a:Type} {a_WT:WhyType a}, (set a).
intros a a_WT.
exact (fun x => true).
Defined.
(* Why3 goal *)
Lemma all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem x
(all :(set a))).
intros a a_WT x.
unfold all,mem; easy.
Qed.
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