Commit 50216dec authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove some obsolete edited proofs.

parent 42d446f6
(* 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 label : Type.
Parameter at1: forall (a:Type), a -> label -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set 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 (set 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).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| mk_array _ elts1 => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| mk_array length1 _ => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Definition eq_board(b1:(array Z)) (b2:(array Z)) (pos:Z): Prop :=
forall (q:Z), ((0%Z <= q)%Z /\ (q < pos)%Z) -> ((get1 b1 q) = (get1 b2
q)).
Axiom eq_board_set : forall (b:(array Z)) (pos:Z) (q:Z) (i:Z),
(pos <= q)%Z -> (eq_board b (set1 b q i) pos).
Axiom eq_board_sym : forall (b1:(array Z)) (b2:(array Z)) (pos:Z),
(eq_board b1 b2 pos) -> (eq_board b2 b1 pos).
Axiom eq_board_trans : forall (b1:(array Z)) (b2:(array Z)) (b3:(array Z))
(pos:Z), (eq_board b1 b2 pos) -> ((eq_board b2 b3 pos) -> (eq_board b1 b3
pos)).
Axiom eq_board_extension : forall (b1:(array Z)) (b2:(array Z)) (pos:Z),
(eq_board b1 b2 pos) -> (((get1 b1 pos) = (get1 b2 pos)) -> (eq_board b1 b2
(pos + 1%Z)%Z)).
Definition consistent_row(board:(array Z)) (pos:Z) (q:Z): Prop :=
(~ ((get1 board q) = (get1 board pos))) /\ ((~ (((get1 board
q) - (get1 board pos))%Z = (pos - q)%Z)) /\ ~ (((get1 board
pos) - (get1 board q))%Z = (pos - q)%Z)).
Axiom consistent_row_eq : forall (b1:(array Z)) (b2:(array Z)) (pos:Z),
(eq_board b1 b2 (pos + 1%Z)%Z) -> forall (q:Z), ((0%Z <= q)%Z /\
(q < pos)%Z) -> ((consistent_row b1 pos q) -> (consistent_row b2 pos q)).
Definition is_consistent(board:(array Z)) (pos:Z): Prop := forall (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> (consistent_row board pos q).
Axiom is_consistent_eq : forall (b1:(array Z)) (b2:(array Z)) (pos:Z),
(eq_board b1 b2 (pos + 1%Z)%Z) -> ((is_consistent b1 pos) ->
(is_consistent b2 pos)).
Definition is_board(board:(array Z)) (pos:Z): Prop := forall (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> ((0%Z <= (get1 board q))%Z /\
((get1 board q) < (length board))%Z).
Definition solution(board:(array Z)) (pos:Z): Prop := (is_board board pos) /\
forall (q:Z), ((0%Z <= q)%Z /\ (q < pos)%Z) -> (is_consistent board q).
Theorem solution_eq_board : forall (b1:(array Z)) (b2:(array Z)) (pos:Z),
((length b1) = (length b2)) -> ((eq_board b1 b2 pos) -> ((solution b1
pos) -> (solution b2 pos))).
(* YOU MAY EDIT THE PROOF BELOW *)
unfold solution, eq_board, is_board, is_consistent; intuition.
rewrite <- H0; generalize (H2 q); auto with *.
rewrite <- H0; generalize (H2 q); auto with *.
unfold consistent_row in *.
assert (hq: (0 <= q < pos)%Z) by omega.
assert (hq0: (0 <= q0 < q)%Z) by omega.
generalize (H3 q hq q0 hq0).
do 2 (rewrite <- H0; try omega).
Qed.
(* DO NOT EDIT BELOW *)
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