Commit bacb2d6a authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

Coq proofs not needed anymore

parent 13f2bc3c
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
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 t : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (t a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (t a b) -> a -> b -> (t a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(t 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:(t a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter create_const: forall (b:Type) (a:Type), b -> (t a b).
Set Contextual Implicit.
Implicit Arguments create_const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (create_const(b1):(t a b)) a1) = b1).
Definition map (a:Type) := (t Z a).
Parameter length: forall (a:Type), (t Z a) -> Z.
Implicit Arguments length.
Axiom Length_non_negative : forall (a:Type), forall (a1:(t Z a)),
(0%Z <= (length a1))%Z.
Axiom Length_set : forall (a:Type), forall (a1:(t Z a)), forall (k:Z),
forall (v:a), ((length (set a1 k v)) = (length a1)).
Parameter create_const_length: forall (a:Type), a -> Z -> (t Z a).
Implicit Arguments create_const_length.
Axiom Create_const_length_get : forall (a:Type), forall (b:a), forall (n:Z)
(i:Z), ((get (create_const_length b n) i) = b).
Axiom Create_const_length_length : forall (a:Type), forall (a1:a),
forall (n:Z), (0%Z <= n)%Z -> ((length (create_const_length a1 n)) = n).
Parameter create_length: forall (a:Type), Z -> (t Z a).
Set Contextual Implicit.
Implicit Arguments create_length.
Unset Contextual Implicit.
Axiom Create_length_length : forall (a:Type), forall (n:Z), (0%Z <= n)%Z ->
((length (create_length(n):(t Z a))) = n).
Parameter array : forall (a:Type), Type.
Definition eq_board(b1:(t Z Z)) (b2:(t Z Z)) (pos:Z): Prop := forall (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> ((get b1 q) = (get b2 q)).
Axiom eq_board_set : forall (b:(t Z Z)) (pos:Z) (q:Z) (i:Z), (pos <= q)%Z ->
(eq_board b (set b q i) pos).
Axiom eq_board_sym : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z), (eq_board b1
b2 pos) -> (eq_board b2 b1 pos).
Axiom eq_board_trans : forall (b1:(t Z Z)) (b2:(t Z Z)) (b3:(t Z Z)) (pos:Z),
(eq_board b1 b2 pos) -> ((eq_board b2 b3 pos) -> (eq_board b1 b3 pos)).
Axiom eq_board_extension : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
(eq_board b1 b2 pos) -> (((get b1 pos) = (get b2 pos)) -> (eq_board b1 b2
(pos + 1%Z)%Z)).
Definition consistent_row(board:(t Z Z)) (pos:Z) (q:Z): Prop :=
(~ ((get board q) = (get board pos))) /\ ((~ (((get board q) - (get board
pos))%Z = (pos - q)%Z)) /\ ~ (((get board pos) - (get board
q))%Z = (pos - q)%Z)).
Axiom consistent_row_eq : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z) (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> ((eq_board b1 b2 (pos + 1%Z)%Z) ->
((consistent_row b1 pos q) -> (consistent_row b2 pos q))).
Definition is_consistent(board:(t Z Z)) (pos:Z): Prop := forall (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> (consistent_row board pos q).
Theorem is_consistent_eq : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
(eq_board b1 b2 (pos + 1%Z)%Z) -> ((is_consistent b1 pos) ->
(is_consistent b2 pos)).
(* YOU MAY EDIT THE PROOF BELOW *)
unfold is_consistent, eq_board.
intros.
apply consistent_row_eq with b1; auto.
Qed.
(* DO NOT EDIT BELOW *)
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
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 t : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (t a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (t a b) -> a -> b -> (t a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(t 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:(t a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter create_const: forall (b:Type) (a:Type), b -> (t a b).
Set Contextual Implicit.
Implicit Arguments create_const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (create_const(b1):(t a b)) a1) = b1).
Definition map (a:Type) := (t Z a).
Parameter length: forall (a:Type), (t Z a) -> Z.
Implicit Arguments length.
Axiom Length_non_negative : forall (a:Type), forall (a1:(t Z a)),
(0%Z <= (length a1))%Z.
Axiom Length_set : forall (a:Type), forall (a1:(t Z a)), forall (k:Z),
forall (v:a), ((length (set a1 k v)) = (length a1)).
Parameter create_const_length: forall (a:Type), a -> Z -> (t Z a).
Implicit Arguments create_const_length.
Axiom Create_const_length_get : forall (a:Type), forall (b:a), forall (n:Z)
(i:Z), ((get (create_const_length b n) i) = b).
Axiom Create_const_length_length : forall (a:Type), forall (a1:a),
forall (n:Z), (0%Z <= n)%Z -> ((length (create_const_length a1 n)) = n).
Parameter create_length: forall (a:Type), Z -> (t Z a).
Set Contextual Implicit.
Implicit Arguments create_length.
Unset Contextual Implicit.
Axiom Create_length_length : forall (a:Type), forall (n:Z), (0%Z <= n)%Z ->
((length (create_length(n):(t Z a))) = n).
Parameter array : forall (a:Type), Type.
Definition eq_board(b1:(t Z Z)) (b2:(t Z Z)) (pos:Z): Prop := forall (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> ((get b1 q) = (get b2 q)).
Axiom eq_board_set : forall (b:(t Z Z)) (pos:Z) (q:Z) (i:Z), (pos <= q)%Z ->
(eq_board b (set b q i) pos).
Axiom eq_board_sym : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z), (eq_board b1
b2 pos) -> (eq_board b2 b1 pos).
Axiom eq_board_trans : forall (b1:(t Z Z)) (b2:(t Z Z)) (b3:(t Z Z)) (pos:Z),
(eq_board b1 b2 pos) -> ((eq_board b2 b3 pos) -> (eq_board b1 b3 pos)).
Axiom eq_board_extension : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
(eq_board b1 b2 pos) -> (((get b1 pos) = (get b2 pos)) -> (eq_board b1 b2
(pos + 1%Z)%Z)).
Definition consistent_row(board:(t Z Z)) (pos:Z) (q:Z): Prop :=
(~ ((get board q) = (get board pos))) /\ ((~ (((get board q) - (get board
pos))%Z = (pos - q)%Z)) /\ ~ (((get board pos) - (get board
q))%Z = (pos - q)%Z)).
Axiom consistent_row_eq : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z) (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> ((eq_board b1 b2 (pos + 1%Z)%Z) ->
((consistent_row b1 pos q) -> (consistent_row b2 pos q))).
Definition is_consistent(board:(t Z 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:(t Z Z)) (b2:(t Z Z)) (pos:Z),
(eq_board b1 b2 (pos + 1%Z)%Z) -> ((is_consistent b1 pos) ->
(is_consistent b2 pos)).
Definition is_board(board:(t Z Z)) (pos:Z): Prop := forall (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> ((0%Z <= (get board q))%Z /\ ((get board
q) < (length board))%Z).
Definition solution(board:(t Z 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:(t Z Z)) (b2:(t Z 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 eq_board, solution, is_board.
intuition.
rewrite <- H0; intuition.
destruct (H2 q); intuition.
rewrite <- H0; intuition.
destruct (H2 q); intuition.
apply is_consistent_eq with b1; intuition.
red; intros.
intuition.
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