n-queens: proof completed

parent a4d0d0fe
......@@ -11,17 +11,13 @@ theory S "finite sets of with succ and pred operations"
function succ (set int) : set int
axiom succ_def_1:
forall s: set int, i: int. mem (i-1) s -> mem i (succ s)
axiom succ_def_2:
forall s: set int, i: int. mem i (succ s) -> i >= 1 -> mem (i-1) s
axiom succ_def:
forall s: set int, i: int. mem i (succ s) <-> i >= 1 /\ mem (i-1) s
function pred (set int) : set int
axiom pred_def_1:
forall s: set int, i: int. mem (i+1) s -> i >= 0 -> mem i (pred s)
axiom pred_def__2:
forall s: set int, i: int. mem i (pred s) -> mem (i+1) s
axiom pred_def:
forall s: set int, i: int. mem i (pred s) <-> i >= 0 /\ mem (i+1) s
end
......@@ -46,7 +42,7 @@ theory Solution
forall i: int. 0 <= i < k ->
0 <= s[i] < n /\
(forall j: int. 0 <= j < i -> s[i] <> s[j] /\
s[i]-s[j] <> i-j /\
s[i]-s[j] <> i-j /\
s[i]-s[j] <> j-i)
predicate solution (s: solution) = partial_solution n s
......@@ -89,13 +85,13 @@ module NQueensSets
!sol[old !s] = !col }
let rec t3 (a b c : set int) variant { cardinal a } =
{ 0 <= !k /\ !k + cardinal a = n /\
{ 0 <= !k /\ !k + cardinal a = n /\ !s >= 0 /\
"pre_a" (forall i: int. mem i a <->
(0<=i<n /\ forall j: int. 0 <= j < !k -> i <> !col[j])) /\
"pre_b" (forall i: int. i>=0 -> mem i b <->
(exists j: int. 0 <= j < !k /\ !col[j] = i + j - !k)) /\
"pre_c" (forall i: int. i>=0 -> mem i c <->
(exists j: int. 0 <= j < !k /\ !col[j] = i + !k - j)) /\
(0<=i<n /\ forall j: int. 0 <= j < !k -> !col[j] <> i)) /\
"pre_b" (forall i: int. i>=0 -> not (mem i b) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + j - !k)) /\
"pre_c" (forall i: int. i>=0 -> not (mem i c) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + !k - j)) /\
partial_solution !k !col }
if not (is_empty a) then begin
let e = ref (diff (diff a b) c) in
......@@ -106,14 +102,15 @@ module NQueensSets
subset !e (at !e 'L) /\
partial_solution !k !col /\
sorted !sol (at !s 'L) !s /\
(forall i j: int. mem i (diff (at !e 'L) !e) -> mem j !e -> i < j) /\
(forall t: solution.
(solution t /\ eq_prefix !col t !k /\
exists di: int. mem di (diff (at !e 'L) !e) /\ t[!k] = di)
<->
(exists i: int. (at !s 'L) <= i < !s /\ eq_sol t !sol[i])) /\
(solution t /\ eq_prefix !col t !k /\ mem t[!k] (diff (at !e 'L) !e))
<->
(exists i: int. (at !s 'L) <= i < !s /\ eq_sol t !sol[i])) /\
(* assigns *)
eq_prefix (at !col 'L) !col (at !k 'L) /\
eq_prefix (at !sol 'L) !sol (at !s 'L) }
variant { cardinal !e }
let d = min_elt !e in
(* ghost *) col := !col[!k <- d];
(* ghost *) incr k;
......@@ -198,6 +195,8 @@ theory Bits "the 1-bits of an integer, as a set of integers"
end
(****
module NQueens
use import Bits
......@@ -270,6 +269,9 @@ module NQueens
subset (bits !e) (at (bits !e) 'L) /\
partial_solution !k !col /\
sorted !sol (at !s 'L) !s /\
(forall i j: int.
mem i (diff (at (bits !e) 'L) (bits !e)) -> mem j (bits !e) ->
i < j) /\
(forall t: solution.
(solution t /\
exists di: int. mem di (diff (at (bits !e) 'L) (bits !e)) /\
......@@ -312,6 +314,8 @@ module NQueens
end
****)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/queens.gui"
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter set : forall (a:Type), Type.
Parameter mem: forall (a:Type), a -> (set a) -> Prop.
Implicit Arguments mem.
Definition infix_eqeq (a:Type)(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) <-> (mem x s2).
Implicit Arguments infix_eqeq.
Axiom extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(infix_eqeq s1 s2) -> (s1 = s2).
Definition subset (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a),
(mem x s1) -> (mem x s2).
Implicit Arguments subset.
Axiom subset_trans : forall (a:Type), forall (s1:(set a)) (s2:(set a))
(s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)).
Parameter empty: forall (a:Type), (set a).
Set Contextual Implicit.
Implicit Arguments empty.
Unset Contextual Implicit.
Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s).
Implicit Arguments is_empty.
Axiom empty_def1 : forall (a:Type), (is_empty (empty:(set a))).
Parameter add: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments add.
Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set a)),
(mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments remove.
Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x
(remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set a)),
(subset (remove x s) s).
Parameter union: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments union.
Axiom union_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments inter.
Axiom inter_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments diff.
Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(subset (diff s1 s2) s1).
Parameter cardinal: forall (a:Type), (set a) -> Z.
Implicit Arguments cardinal.
Axiom cardinal_nonneg : forall (a:Type), forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall (a:Type), forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall (a:Type), forall (x:a), forall (s:(set a)),
(~ (mem x s)) -> ((cardinal (add x s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall (a:Type), forall (x:a), forall (s:(set a)),
(mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).
Axiom cardinal_subset : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Parameter min_elt: (set Z) -> Z.
Axiom min_elt_def1 : forall (s:(set Z)), (~ (is_empty s)) -> (mem (min_elt s)
s).
Axiom min_elt_def2 : forall (s:(set Z)), (~ (is_empty s)) -> forall (x:Z),
(mem x s) -> ((min_elt s) <= x)%Z.
Parameter max_elt: (set Z) -> Z.
Axiom max_elt_def1 : forall (s:(set Z)), (~ (is_empty s)) -> (mem (max_elt s)
s).
Axiom max_elt_def2 : forall (s:(set Z)), (~ (is_empty s)) -> forall (x:Z),
(mem x s) -> (x <= (max_elt s))%Z.
Parameter below: Z -> (set Z).
Axiom below_def : forall (x:Z) (n:Z), (mem x (below n)) <-> ((0%Z <= x)%Z /\
(x < n)%Z).
Axiom cardinal_below : forall (n:Z), ((0%Z <= n)%Z ->
((cardinal (below n)) = n)) /\ ((~ (0%Z <= n)%Z) ->
((cardinal (below n)) = 0%Z)).
Parameter succ: (set Z) -> (set Z).
Axiom succ_def : forall (s:(set Z)) (i:Z), (mem i (succ s)) <->
((1%Z <= i)%Z /\ (mem (i - 1%Z)%Z s)).
Parameter pred: (set Z) -> (set Z).
Axiom pred_def : forall (s:(set Z)) (i:Z), (mem i (pred s)) <->
((0%Z <= i)%Z /\ (mem (i + 1%Z)%Z s)).
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set1: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set1.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set1 m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set1 m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Parameter n: Z.
Definition solution := (map Z Z).
Definition eq_prefix (a:Type)(t:(map Z a)) (u:(map Z a)) (i:Z): Prop :=
forall (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) -> ((get t k) = (get u k)).
Implicit Arguments eq_prefix.
Definition partial_solution(k:Z) (s:(map Z Z)): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < k)%Z) -> (((0%Z <= (get s i))%Z /\ ((get s
i) < (n ))%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ((~ ((get s
i) = (get s j))) /\ ((~ (((get s i) - (get s j))%Z = (i - j)%Z)) /\
~ (((get s i) - (get s j))%Z = (j - i)%Z)))).
Axiom partial_solution_eq_prefix : forall (u:(map Z Z)) (t:(map Z Z)) (k:Z),
(partial_solution k t) -> ((eq_prefix t u k) -> (partial_solution k u)).
Definition lt_sol(s1:(map Z Z)) (s2:(map Z Z)): Prop := exists i:Z,
((0%Z <= i)%Z /\ (i < (n ))%Z) /\ ((eq_prefix s1 s2 i) /\ ((get s1
i) < (get s2 i))%Z).
Definition solutions := (map Z (map Z Z)).
Definition sorted(s:(map Z (map Z Z))) (a:Z) (b:Z): Prop := forall (i:Z)
(j:Z), (((a <= i)%Z /\ (i < j)%Z) /\ (j < b)%Z) -> (lt_sol (get s i)
(get s j)).
Parameter col: (ref (map Z Z)).
Parameter k: (ref Z).
Parameter sol: (ref (map Z (map Z Z))).
Parameter s: (ref Z).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_t3 : forall (a:(set Z)), forall (b:(set Z)),
forall (c:(set Z)), forall (s1:Z), forall (sol1:(map Z (map Z Z))),
forall (k1:Z), forall (col1:(map Z Z)), ((0%Z <= k1)%Z /\
(((k1 + (cardinal a))%Z = (n )) /\ ((0%Z <= s1)%Z /\ ((forall (i:Z), (mem i
a) <-> (((0%Z <= i)%Z /\ (i < (n ))%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < k1)%Z) -> ~ ((get col1 j) = i))) /\ ((forall (i:Z), (0%Z <= i)%Z ->
((~ (mem i b)) <-> forall (j:Z), ((0%Z <= j)%Z /\ (j < k1)%Z) ->
~ ((get col1 j) = ((i + j)%Z - k1)%Z))) /\ ((forall (i:Z), (0%Z <= i)%Z ->
((~ (mem i c)) <-> forall (j:Z), ((0%Z <= j)%Z /\ (j < k1)%Z) ->
~ ((get col1 j) = ((i + k1)%Z - j)%Z))) /\ (partial_solution k1
col1))))))) -> ((~ (is_empty a)) -> forall (f:Z), forall (e:(set Z)),
forall (s2:Z), forall (sol2:(map Z (map Z Z))), forall (k2:Z),
forall (col2:(map Z Z)), (((f = (s2 - s1)%Z) /\ (0%Z <= (s2 - s1)%Z)%Z) /\
((k2 = k1) /\ ((subset e (diff (diff a b) c)) /\ ((partial_solution k2
col2) /\ ((sorted sol2 s1 s2) /\ ((forall (i:Z) (j:Z), (mem i
(diff (diff (diff a b) c) e)) -> ((mem j e) -> (i < j)%Z)) /\
((forall (t:(map Z Z)), ((partial_solution (n ) t) /\ ((eq_prefix col2 t
k2) /\ (mem (get t k2) (diff (diff (diff a b) c) e)))) <-> exists i:Z,
((s1 <= i)%Z /\ (i < s2)%Z) /\ (eq_prefix t (get sol2 i) (n ))) /\
((eq_prefix col1 col2 k1) /\ (eq_prefix sol1 sol2 s1))))))))) ->
((~ (is_empty e)) -> forall (col3:(map Z Z)), (col3 = (set1 col2 k2
(min_elt e))) -> forall (k3:Z), (k3 = (k2 + 1%Z)%Z) -> forall (i:Z),
(((0%Z <= i)%Z /\ (i < (n ))%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < k3)%Z) -> ~ ((get col3 j) = i)) -> (mem i (remove (min_elt e) a)))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
generalize (remove_def1 _ i (min_elt e) a); intuition.
assert (case: (i = min_elt e \/ i<> min_elt e)%Z) by omega. destruct case.
elim H22 with k2.
omega.
subst col3; rewrite Select_eq; auto.
apply H21; auto.
destruct (H3 i) as (_,h); apply h; intuition.
apply H22 with j; try omega.
subst col3; rewrite Select_neq; try omega.
rewrite <- H16; try omega.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -136,20 +136,14 @@ Axiom cardinal_below : forall (n:Z), ((0%Z <= n)%Z ->
Parameter succ: (set Z) -> (set Z).
Axiom succ_def_1 : forall (s:(set Z)) (i:Z), (mem (i - 1%Z)%Z s) -> (mem i
(succ s)).
Axiom succ_def_2 : forall (s:(set Z)) (i:Z), (mem i (succ s)) ->
((1%Z <= i)%Z -> (mem (i - 1%Z)%Z s)).
Axiom succ_def : forall (s:(set Z)) (i:Z), (mem i (succ s)) <->
((1%Z <= i)%Z /\ (mem (i - 1%Z)%Z s)).
Parameter pred: (set Z) -> (set Z).
Axiom pred_def_1 : forall (s:(set Z)) (i:Z), (mem (i + 1%Z)%Z s) ->
((0%Z <= i)%Z -> (mem i (pred s))).
Axiom pred_def__2 : forall (s:(set Z)) (i:Z), (mem i (pred s)) ->
(mem (i + 1%Z)%Z s).
Axiom pred_def : forall (s:(set Z)) (i:Z), (mem i (pred s)) <->
((0%Z <= i)%Z /\ (mem (i + 1%Z)%Z s)).
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
......@@ -235,24 +229,26 @@ Parameter s: (ref Z).
Theorem WP_parameter_t3 : forall (a:(set Z)), forall (b:(set Z)),
forall (c:(set Z)), forall (s1:Z), forall (sol1:(map Z (map Z Z))),
forall (k1:Z), forall (col1:(map Z Z)), ((0%Z <= k1)%Z /\
(((k1 + (cardinal a))%Z = (n )) /\ ((forall (i:Z), (mem i a) <->
(((0%Z <= i)%Z /\ (i < (n ))%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < k1)%Z) -> ~ (i = (get col1 j)))) /\ ((forall (i:Z), (0%Z <= i)%Z ->
((mem i b) <-> exists j:Z, ((0%Z <= j)%Z /\ (j < k1)%Z) /\ ((get col1
j) = ((i + j)%Z - k1)%Z))) /\ ((forall (i:Z), (0%Z <= i)%Z -> ((mem i
c) <-> exists j:Z, ((0%Z <= j)%Z /\ (j < k1)%Z) /\ ((get col1
j) = ((i + k1)%Z - j)%Z))) /\ (partial_solution k1 col1)))))) ->
((~ (is_empty a)) -> forall (f:Z), forall (e:(set Z)), forall (s2:Z),
forall (sol2:(map Z (map Z Z))), forall (k2:Z), forall (col2:(map Z Z)),
(((f = (s2 - s1)%Z) /\ (0%Z <= (s2 - s1)%Z)%Z) /\ ((k2 = k1) /\ ((subset e
(diff (diff a b) c)) /\ ((partial_solution k2 col2) /\ ((sorted sol2 s1
s2) /\ ((forall (t:(map Z Z)), ((partial_solution (n ) t) /\
((eq_prefix col2 t k2) /\ exists di:Z, (mem di (diff (diff (diff a b) c)
e)) /\ ((get t k2) = di))) <-> exists i:Z, ((s1 <= i)%Z /\ (i < s2)%Z) /\
(eq_prefix t (get sol2 i) (n ))) /\ ((eq_prefix col1 col2 k1) /\
(eq_prefix sol1 sol2 s1)))))))) -> ((is_empty e) -> forall (t:(map Z Z)),
((partial_solution (n ) t) /\ (eq_prefix col2 t k2)) -> exists i:Z,
((s1 <= i)%Z /\ (i < s2)%Z) /\ (eq_prefix t (get sol2 i) (n )))).
(((k1 + (cardinal a))%Z = (n )) /\ ((0%Z <= s1)%Z /\ ((forall (i:Z), (mem i
a) <-> (((0%Z <= i)%Z /\ (i < (n ))%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < k1)%Z) -> ~ ((get col1 j) = i))) /\ ((forall (i:Z), (0%Z <= i)%Z ->
((~ (mem i b)) <-> forall (j:Z), ((0%Z <= j)%Z /\ (j < k1)%Z) ->
~ ((get col1 j) = ((i + j)%Z - k1)%Z))) /\ ((forall (i:Z), (0%Z <= i)%Z ->
((~ (mem i c)) <-> forall (j:Z), ((0%Z <= j)%Z /\ (j < k1)%Z) ->
~ ((get col1 j) = ((i + k1)%Z - j)%Z))) /\ (partial_solution k1
col1))))))) -> ((~ (is_empty a)) -> forall (f:Z), forall (e:(set Z)),
forall (s2:Z), forall (sol2:(map Z (map Z Z))), forall (k2:Z),
forall (col2:(map Z Z)), (((f = (s2 - s1)%Z) /\ (0%Z <= (s2 - s1)%Z)%Z) /\
((k2 = k1) /\ ((subset e (diff (diff a b) c)) /\ ((partial_solution k2
col2) /\ ((sorted sol2 s1 s2) /\ ((forall (i:Z) (j:Z), (mem i
(diff (diff (diff a b) c) e)) -> ((mem j e) -> (i < j)%Z)) /\
((forall (t:(map Z Z)), ((partial_solution (n ) t) /\ ((eq_prefix col2 t
k2) /\ (mem (get t k2) (diff (diff (diff a b) c) e)))) <-> exists i:Z,
((s1 <= i)%Z /\ (i < s2)%Z) /\ (eq_prefix t (get sol2 i) (n ))) /\
((eq_prefix col1 col2 k1) /\ (eq_prefix sol1 sol2 s1))))))))) ->
((is_empty e) -> forall (t:(map Z Z)), ((partial_solution (n ) t) /\
(eq_prefix col2 t k2)) -> exists i:Z, ((s1 <= i)%Z /\ (i < s2)%Z) /\
(eq_prefix t (get sol2 i) (n )))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
subst k2. rename k1 into k.
......@@ -263,27 +259,44 @@ intuition.
assert (case: (cardinal a = 0 \/ cardinal a > 0)%Z) by omega. destruct case.
absurd (is_empty a); auto.
omega.
destruct (H13 t) as (h1,_); clear H13.
destruct (H15 t) as (h1,_).
apply h1; intuition.
exists (get t k); intuition.
destruct (diff_def1 _ (diff (diff a b) c) e (get t k)) as (_, h); apply h; clear h; split.
destruct (diff_def1 _ (diff a b) c (get t k)) as (_, h); apply h; clear h; split.
destruct (diff_def1 _ a b (get t k)) as (_, h); apply h; clear h; split.
(* mem .. a *)
destruct (H2 (get t k)) as (_,h); apply h; clear h.
destruct (H3 (get t k)) as (_,h); apply h; clear h.
split.
destruct (H17 k) as (h,_).
destruct (H19 k) as (h,_).
omega.
assumption.
intros j hj.
rewrite H14.
rewrite H18.
destruct (H17 k) as (_,h). omega.
rewrite H16.
rewrite H20.
destruct (H19 k) as (_,h). omega.
destruct (h j); intuition.
assumption.
assumption.
(* not (mem ... b) *)
destruct (H4 (get t k)) as (_,h).
destruct (H19 k); omega.
red; intro h1; apply h; clear h; auto.
intros j hj.
rewrite H16; try omega.
rewrite H20; try omega.
destruct (H19 k); intuition.
destruct (H22 j); intuition.
(* not (mem ... c) *)
destruct (H5 (get t k)) as (_,h).
destruct (H19 k); omega.
red; intro h1; apply h; clear h; auto.
intros j hj.
rewrite H16; try omega.
rewrite H20; try omega.
destruct (H19 k); intuition.
destruct (H22 j); intuition.
(* not (mem ... e) *)
apply H8.
Qed.
(* DO NOT EDIT BELOW *)
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter set : forall (a:Type), Type.
Parameter mem: forall (a:Type), a -> (set a) -> Prop.
Implicit Arguments mem.
Definition infix_eqeq (a:Type)(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) <-> (mem x s2).
Implicit Arguments infix_eqeq.
Axiom extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(infix_eqeq s1 s2) -> (s1 = s2).
Definition subset (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a),
(mem x s1) -> (mem x s2).
Implicit Arguments subset.
Axiom subset_trans : forall (a:Type), forall (s1:(set a)) (s2:(set a))
(s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)).
Parameter empty: forall (a:Type), (set a).
Set Contextual Implicit.
Implicit Arguments empty.
Unset Contextual Implicit.
Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s).
Implicit Arguments is_empty.
Axiom empty_def1 : forall (a:Type), (is_empty (empty:(set a))).
Parameter add: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments add.
Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set a)),
(mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments remove.
Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x
(remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set a)),
(subset (remove x s) s).
Parameter union: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments union.
Axiom union_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments inter.
Axiom inter_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments diff.
Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(subset (diff s1 s2) s1).
Parameter cardinal: forall (a:Type), (set a) -> Z.
Implicit Arguments cardinal.
Axiom cardinal_nonneg : forall (a:Type), forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall (a:Type), forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall (a:Type), forall (x:a), forall (s:(set a)),
(~ (mem x s)) -> ((cardinal (add x s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall (a:Type), forall (x:a), forall (s:(set a)),
(mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).
Axiom cardinal_subset : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Parameter min_elt: (set Z) -> Z.