edit_distance_Word_key_lemma_right_1.v 3.08 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
3 4 5 6
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
7 8 9 10
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
11

12 13
Axiom char : Type.
Parameter char_WhyType : WhyType char.
14
Existing Instance char_WhyType.
15

16
(* Why3 assumption *)
17
Definition word := (list char).
18 19

(* Why3 assumption *)
20 21 22 23 24 25 26 27
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
  | dist_eps : (dist nil nil 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).
28 29

(* Why3 assumption *)
30 31
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.
32

33
(* Why3 assumption *)
34
Fixpoint last_char (a:char) (u:(list char)) {struct u}: char :=
35
  match u with
36 37
  | nil => a
  | (cons c u') => (last_char c u')
38 39
  end.

40
(* Why3 assumption *)
41
Fixpoint but_last (a:char) (u:(list char)) {struct u}: (list char) :=
42
  match u with
43 44
  | nil => nil
  | (cons c u') => (cons a (but_last c u'))
45 46 47
  end.

Axiom first_last_explicit : forall (u:(list char)) (a:char),
48
  ((List.app (but_last a u) (cons (last_char a u) nil)) = (cons a u)).
49 50

Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
51 52
  exists b:char, ((List.app v (cons b nil)) = (cons a u)) /\
  ((list.Length.length v) = (list.Length.length u)).
53

54 55
Lemma app_comm_cons: forall {A:Type} {A_WT:WhyType A} (x y : list A) (a: A),
   cons a (app x y) = app (cons a x) y.
56 57 58
simpl; auto.
Qed.

59
(* Why3 goal *)
60 61 62 63 64 65
Theorem 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 = (List.app u1 v1)) /\ ((dist v1 w2 k) /\
  ((k + (list.Length.length u1))%Z <= (m + 1%Z)%Z)%Z).
(* Why3 intros w1 w'2 m a h1 w2 h2. *)
66 67 68 69 70 71 72 73 74 75 76
intros w1 w'2 m a H; elim H.
(* 1. [dist_eps]: absurd *)
intros; discriminate H0.
(* 2. [dist_add_left]: we use induction hypothesis. *)
intros w'1 w3 n Hdist Hrec b w2 Heq.
  elim (Hrec w2 Heq); intros u'1 Hex.
elim Hex; clear Hex; intros v'1 Hex.
elim Hex; clear Hex; intros k Hex.
decompose [and] Hex; clear Hex.
elim (first_last b u'1); intros u1 Hex.
elim Hex; intros c [Hc Hlength].
77
exists u1; exists (cons c v'1); exists (k + 1)%Z.
78 79 80 81
repeat split.
rewrite H0.
rewrite app_comm_cons.
rewrite <- Hc.
82
rewrite <- Append.Append_assoc; reflexivity.
83 84 85 86
apply dist_add_left; assumption.
omega.
(* 3. [dist_add_right]: direct *)
intros.
87
exists nil; exists w0; exists n.
88 89 90 91 92 93 94
repeat split.
inversion H2.
rewrite <- H5; assumption.
simpl; omega.
(* 4. [dist_context]: direct *)
intros.
inversion H2.
95
exists (cons a nil); exists w0; exists n.
96 97 98 99 100 101
repeat split.
rewrite <- H5; assumption.
simpl; omega.
Qed.