Commit 1ce76bcc authored by Guillaume Melquiond's avatar Guillaume Melquiond

Handle implicit arguments uniformly inside Coq printer.

parent 0c9795cf
......@@ -2,56 +2,37 @@
(* 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.
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)).
Require int.Int.
Require int.MinMax.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
(* Why3 assumption *)
Fixpoint length {a:Type}(l:(list a)) {struct l}: Z :=
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)),
Axiom Length_nonnegative : forall {a:Type}, 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}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Parameter char : Type.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
| 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
......@@ -59,68 +40,65 @@ Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| 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).
(* Why3 assumption *)
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
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type}(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))
Axiom Append_assoc : forall {a:Type}, 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}, forall (l:(list a)), ((infix_plpl l
(Nil :(list a))) = l).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
Axiom Append_length : forall {a:Type}, 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}(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)),
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_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
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))).
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)).
Axiom 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
Axiom key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:Z)
(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:Z,
(w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
......@@ -133,20 +111,18 @@ Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
char), exists k:Z, (w2 = (infix_plpl u2 v2)) /\ ((dist w1 v2 k) /\
((k + (length u2))%Z <= (m + 1%Z)%Z)%Z).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Theorem dist_concat_left : forall (u:(list char)) (v:(list char)) (w:(list
char)) (n:Z), (dist v w n) -> (dist (infix_plpl u v) w ((length u) + n)%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
simple induction u; intros.
auto.
unfold length; fold length.
unfold length; fold @length.
replace (1 + length l + n)%Z with (length l + n + 1)%Z;
[ idtac | omega ].
apply dist_add_left; auto.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -2,56 +2,37 @@
(* 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.
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)).
Require int.Int.
Require int.MinMax.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
(* Why3 assumption *)
Fixpoint length {a:Type}(l:(list a)) {struct l}: Z :=
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)),
Axiom Length_nonnegative : forall {a:Type}, 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}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Parameter char : Type.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
| 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
......@@ -59,68 +40,64 @@ Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| 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).
(* Why3 assumption *)
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
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type}(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))
Axiom Append_assoc : forall {a:Type}, 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}, forall (l:(list a)), ((infix_plpl l
(Nil :(list a))) = l).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
Axiom Append_length : forall {a:Type}, 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}(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)),
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_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
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))).
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)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Theorem 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 PROOF BELOW *)
intros a u.
......@@ -131,9 +108,8 @@ split.
generalize a; induction u; intros.
simpl; omega.
unfold but_last; fold but_last.
unfold length; fold length.
unfold length; fold @length.
generalize (IHu a0); intros; omega.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -2,56 +2,37 @@
(* 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.
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)).
Require int.Int.
Require int.MinMax.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
(* Why3 assumption *)
Fixpoint length {a:Type}(l:(list a)) {struct l}: Z :=
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)),
Axiom Length_nonnegative : forall {a:Type}, 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}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Parameter char : Type.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z)
| 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
......@@ -59,9 +40,83 @@ Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| 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).
(* Why3 assumption *)
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.
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type}(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type}, 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_length : forall {a:Type}, forall (l1:(list a)) (l2:(list a)),
((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
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_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))).
(* Why3 assumption *)
Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
match u with
| Nil => a
| (Cons c u') => (last_char c u')
end.
(* Why3 assumption *)
Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
match u with
| Nil => (Nil :(list char))
| (Cons c u') => (Cons a (but_last c u'))
end.
Axiom first_last_explicit : forall (u:(list char)) (a:char),
((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)) /\
((length v) = (length u)).
Axiom key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:Z)
(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:Z,
(w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> (dist w2 w1 n).
Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
(a:char), (dist (Cons a w1) w2 m) -> exists u2:(list char), exists v2:(list
char), exists k:Z, (w2 = (infix_plpl u2 v2)) /\ ((dist w1 v2 k) /\
((k + (length u2))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_concat_left : forall (u:(list char)) (v:(list char)) (w:(list
char)) (n:Z), (dist v w n) -> (dist (infix_plpl u v) w ((length u) + n)%Z).
Axiom dist_concat_right : forall (u:(list char)) (v:(list char)) (w:(list
char)) (n:Z), (dist v w n) -> (dist v (infix_plpl u w) ((length u) + n)%Z).
Axiom min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char)
(n:Z), (min_dist w1 w2 n) -> (min_dist (Cons a w1) (Cons a w2) n).
......@@ -71,16 +126,18 @@ Axiom min_dist_diff : forall (w1:(list char)) (w2:(list char)) (a:char)
((Zmin m p) + 1%Z)%Z))).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w
(Nil:(list char)) n) -> (min_dist (Cons a w) (Nil:(list char))
(Nil :(list char)) n) -> (min_dist (Cons a w) (Nil :(list char))
(n + 1%Z)%Z).
Theorem min_dist_eps_length : forall (w:(list char)), (min_dist (Nil:(list
(* Why3 goal *)
Theorem min_dist_eps_length : forall (w:(list char)), (min_dist (Nil :(list
char)) w (length w)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros w; unfold min_dist; intuition.
induction w; intros.
exact dist_eps.
unfold length; fold length.
unfold length; fold @length.
replace (1 + length w)%Z with (length w + 1)%Z by omega.
apply dist_add_right; assumption.
generalize m H.
......@@ -88,9 +145,8 @@ generalize m H.
induction w; intros m H; inversion H.
simpl; omega.
generalize (IHw n H4); intro; try omega.
unfold length; fold length.
unfold length; fold @length.
omega.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -2,187 +2,166 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.