Commit ebd056a5 by Guillaume Melquiond

### Fix some user parts in Coq proofs.

`Almost all of them are one-liner changes to account for the additional hypotheses.`
parent e4eaa5ca
This diff is collapsed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\ (y <= (Zmax x y))%Z. Require Import BuiltIn. Require BuiltIn. Require int.Int. Require int.MinMax. Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y). Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\ ((Zmin x y) <= y)%Z. Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y). Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x). Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y). Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x). Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y). Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)). Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)). Inductive list (a:Type) := (* Why3 assumption *) Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. (* Why3 assumption *) Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: BuiltIn.int := match l with | Nil => 0%Z | Cons _ r => (1%Z + (length r))%Z | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). Parameter char : Type. Axiom char_WhyType : WhyType char. Existing Instance char_WhyType. (* Why3 assumption *) Definition word := (list char). Inductive dist : (list char) -> (list char) -> Z -> Prop := | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z) | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z) | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z) | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n). Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1 w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z. Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := (* Why3 assumption *) Inductive dist : (list char) -> (list char) -> BuiltIn.int -> Prop := | dist_eps : (dist (Nil :(list char)) (Nil :(list char)) 0%Z) | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:BuiltIn.int), (dist w1 w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z) | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:BuiltIn.int), (dist w1 w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z) | dist_context : forall (w1:(list char)) (w2:(list char)) (n:BuiltIn.int), (dist w1 w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n). (* Why3 assumption *) Definition min_dist(w1:(list char)) (w2:(list char)) (n:BuiltIn.int): Prop := (dist w1 w2 n) /\ forall (m:BuiltIn.int), (dist w1 w2 m) -> (n <= m)%Z. (* Why3 assumption *) Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | Cons x1 r1 => (Cons x1 (infix_plpl r1 l2)) | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l (Nil:(list a))) = l). Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((infix_plpl l (Nil :(list a))) = l). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := (* Why3 assumption *) Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | Cons y r => (x = y) \/ (mem x r) | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Set Implicit Arguments. (* Why3 assumption *) Fixpoint last_char(a:char) (u:(list char)) {struct u}: char := match u with | Nil => a | Cons c uqt => (last_char c uqt) | Nil => a | (Cons c u') => (last_char c u') end. Unset Implicit Arguments. Set Implicit Arguments. (* Why3 assumption *) Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) := match u with | Nil => (Nil:(list char)) | Cons c uqt => (Cons a (but_last c uqt)) | Nil => (Nil :(list char)) | (Cons c u') => (Cons a (but_last c u')) end. Unset Implicit Arguments. Axiom first_last_explicit : forall (u:(list char)) (a:char), ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil:(list ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil :(list char)))) = (Cons a u)). Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char), exists b:char, ((infix_plpl v (Cons b (Nil:(list char)))) = (Cons a u)) /\ exists b:char, ((infix_plpl v (Cons b (Nil :(list char)))) = (Cons a u)) /\ ((length v) = (length u)). (* YOU MAY EDIT THE CONTEXT BELOW *) Lemma app_comm_cons: forall (A:Type) (x y : list A) (a: A), Lemma app_comm_cons: forall (A:Type) {A_WT:WhyType A} (x y : list A) (a: A), Cons a (infix_plpl x y) = infix_plpl (Cons a x) y. simpl; auto. Qed. (* DO NOT EDIT BELOW *) Theorem key_lemma_right : forall (w1:(list char)) (wqt2:(list char)) (m:Z) (a:char), (dist w1 wqt2 m) -> forall (w2:(list char)), (wqt2 = (Cons a w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z, (w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\ (* Why3 goal *) Theorem key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:BuiltIn.int) (a:char), (dist w1 w'2 m) -> forall (w2:(list char)), (w'2 = (Cons a w2)) -> exists u1:(list char), exists v1:(list char), exists k:BuiltIn.int, (w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\ ((k + (length u1))%Z <= (m + 1%Z)%Z)%Z). (* YOU MAY EDIT THE PROOF BELOW *) intros w1 w'2 m a H; elim H. ... ... @@ -166,6 +152,5 @@ repeat split. rewrite <- H5; assumption. simpl; omega. 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. Require Import BuiltIn. Require Import ZOdiv. Require BuiltIn. Require int.Int. Require int.Abs. Require int.ComputerDivision. ... ... @@ -11,155 +11,154 @@ Require int.ComputerDivision. Definition unit := unit. (* Why3 assumption *) Inductive option (a:Type) := Inductive option (a:Type) {a_WT:WhyType a} := | None : option a | Some : a -> option a. Set Contextual Implicit. Implicit Arguments None. Unset Contextual Implicit. Implicit Arguments Some. Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a). Existing Instance option_WhyType. Implicit Arguments None [[a] [a_WT]]. Implicit Arguments Some [[a] [a_WT]]. Parameter map : forall (a:Type) (b:Type), Type. Parameter map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. Axiom map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b). Existing Instance map_WhyType. Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. Implicit Arguments get. Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b. Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). Implicit Arguments set. Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b -> (map a b). 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_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, 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)). Axiom Select_neq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, 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 (a:Type) (b:Type), b -> (map a b). Set Contextual Implicit. Implicit Arguments const. Unset Contextual Implicit. Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, b -> (map a b). Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). (* Why3 assumption *) Inductive list (a:Type) := Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. (* Why3 assumption *) Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. (* Why3 assumption *) Inductive array (a:Type) := | mk_array : Z -> (map Z a) -> array a. Implicit Arguments mk_array. Inductive array (a:Type) {a_WT:WhyType a} := | mk_array : BuiltIn.int -> (map BuiltIn.int a) -> array a. Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a). Existing Instance array_WhyType. Implicit Arguments mk_array [[a] [a_WT]]. (* Why3 assumption *) Definition elts (a:Type)(v:(array a)): (map Z a) := match v with Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map BuiltIn.int a) := match v with | (mk_array x x1) => x1 end. Implicit Arguments elts. (* Why3 assumption *) Definition length (a:Type)(v:(array a)): Z := Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): BuiltIn.int := match v with | (mk_array x x1) => x end. Implicit Arguments length. (* Why3 assumption *) Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). Implicit Arguments get1. Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int): a := (get (elts a1) i). (* Why3 assumption *) Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := (mk_array (length a1) (set (elts a1) i v)). Implicit Arguments set1. Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int) (v:a): (array a) := (mk_array (length a1) (set (elts a1) i v)). (* Why3 assumption *) Inductive t (a:Type) (b:Type) := Inductive t (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b} := | mk_t : (map a (option b)) -> (array (list (a* b)%type)) -> t a b. Implicit Arguments mk_t. Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (t a b). Existing Instance t_WhyType. Implicit Arguments mk_t [[a] [a_WT] [b] [b_WT]]. (* Why3 assumption *) Definition data (a:Type) (b:Type)(v:(t a b)): (array (list (a* b)%type)) := match v with Definition data {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}(v:(t a b)): (array (list (a* b)%type)) := match v with | (mk_t x x1) => x1 end. Implicit Arguments data. (* Why3 assumption *) Definition contents (a:Type) (b:Type)(v:(t a b)): (map a (option b)) := match v with Definition contents {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}(v:(t a b)): (map a (option b)) := match v with | (mk_t x x1) => x end. Implicit Arguments contents. (* Why3 assumption *) Definition get2 (a:Type) (b:Type)(h:(t a b)) (k:a): (option b) := (get (contents h) k). Implicit Arguments get2. Definition get2 {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}(h:(t a b)) (k:a): (option b) := (get (contents h) k). Parameter hash: forall (a:Type), a -> Z. Implicit Arguments hash. Parameter hash: forall {a:Type} {a_WT:WhyType a}, a -> BuiltIn.int. (* Why3 assumption *) Definition idx (a:Type) (b:Type)(h:(t a b)) (k:a): Z := (ZOmod (Zabs (hash k)) (length (data h))). Implicit Arguments idx. Definition idx {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}(h:(t a b)) (k:a): BuiltIn.int := (ZOmod (Zabs (hash k)) (length (data h))). (* Why3 assumption *) Set Implicit Arguments. Fixpoint occurs_first (a:Type) (b:Type)(k:a) (v:b) (l:(list (a* Fixpoint occurs_first {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}(k:a) (v:b) (l:(list (a* b)%type)) {struct l}: Prop := match l with | Nil => False | (Cons (k', v') r) => ((k = k') /\ (v = v')) \/ ((~ (k = k')) /\ (occurs_first k v r)) end. Unset Implicit Arguments. Axiom mem_occurs_first : forall (a:Type) (b:Type), forall (k:a) (v:b) (l:(list (a* b)%type)), (occurs_first k v l) -> (mem (k, v) l). Axiom mem_occurs_first : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (k:a) (v:b) (l:(list (a* b)%type)), (occurs_first k v l) -> (mem (k, v) l). Axiom cons_occurs_first : forall (a:Type) (b:Type), forall (k1:a) (v1:b) (l:(list (a* b)%type)), (occurs_first k1 v1 l) -> forall (k:a) (v:b), (~ (k = k1)) -> (occurs_first k1 v1 (Cons (k, v) l)). Axiom cons_occurs_first : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (k1:a) (v1:b) (l:(list (a* b)%type)), (occurs_first k1 v1 l) -> forall (k:a) (v:b), (~ (k = k1)) -> (occurs_first k1 v1 (Cons (k, v) l)). (* Why3 assumption *) Definition valid (a:Type) (b:Type)(h:(t a b)): Prop := (0%Z < (length (data h)))%Z /\ ((forall (k:a) (v:b), ((get2 h Definition valid {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}(h:(t a b)): Prop := (0%Z < (length (data h)))%Z /\ ((forall (k:a) (v:b), ((get2 h k) = (Some v)) <-> (occurs_first k v (get1 (data h) (idx h k)))) /\ forall (k:a) (v:b), forall (i:Z), ((0%Z <= i)%Z /\ forall (k:a) (v:b), forall (i:BuiltIn.int), ((0%Z <= i)%Z /\ (i < (length (data h)))%Z) -> ((mem (k, v) (get1 (data h) i)) -> (i = (idx h k)))). Implicit Arguments valid. Axiom idx_bounds : forall (a:Type) (b:Type), forall (h:(t a b)), (valid h) -> forall (k:a), (0%Z <= (idx h k))%Z /\ ((idx h k) < (length (data h)))%Z. Axiom idx_bounds : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (h:(t a b)), (valid h) -> forall (k:a), (0%Z <= (idx h k))%Z /\ ((idx h k) < (length (data h)))%Z. (* Why3 goal *) Theorem WP_parameter_find : forall (a:Type) (b:Type), forall (h:Z) (k:a), forall (rho:(map Z (list (a* b)%type))) (rho1:(map a (option b))), Theorem WP_parameter_find : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (h:BuiltIn.int) (k:a), forall (rho:(map BuiltIn.int (list (a* b)%type))) (rho1:(map a (option b))), (valid (mk_t rho1 (mk_array h rho))) -> let i := (ZOmod (Zabs (hash k)) h) in (((0%Z <= i)%Z /\ (i < h)%Z) -> ((forall (v:b), ~ (mem (k, v) (get rho i))) -> ((get rho1 k) = (None :(option b))))). intros a b h k rho rho1. intros a _a b _b h k rho rho1. unfold valid. pose (i := (Zabs (hash k) mod h)). unfold get1; simpl. ... ...
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import BuiltIn. Require BuiltIn. Require int.Int. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive list (a:Type) := Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Implicit Arguments Nil [[a]]. Implicit Arguments Cons [[a]]. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. Parameter head: forall {a:Type}, (list a) -> a. Parameter head: forall {a:Type} {a_WT:WhyType a}, (list a) -> a. Axiom head_cons : forall {a:Type}, forall (x:a) (l:(list a)), ((head (Cons x l)) = x). Axiom head_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), ((head (Cons x l)) = x). Parameter tail: forall {a:Type}, (list a) -> (list a). Parameter tail: forall {a:Type} {a_WT:WhyType a}, (list a) -> (list a). Axiom tail_cons : forall {a:Type}, forall (x:a) (l:(list a)), ((tail (Cons x l)) = l). Axiom tail_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), ((tail (Cons x l)) = l). (* Why3 assumption *) Fixpoint mem {a:Type}(x:a) (l:(list a)) {struct l}: Prop := Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. (* Why3 assumption *)