kmp: proof in progress

parent c4f4867e
......@@ -98,7 +98,7 @@ module KnuthMorrisPratt
val next : array int
let initnext () =
{ length next = length p }
{ 1 <= length next = length p }
let m = length p in
let i = ref 1 in
let j = ref 0 in
......@@ -128,7 +128,7 @@ module KnuthMorrisPratt
(forall k: int. 0 <= k < r -> not (matches a k p 0 (length p)))
let kmp (a: array char) =
{ length next = length p }
{ 1 <= length next = length p /\ 0 <= length a }
let m = length p in
let n = length a in
let i = ref 0 in
......
(* 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 mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
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.
Parameter char : Type.
Definition matches(a1:(array char)) (i1:Z) (a2:(array char)) (i2:Z)
(n:Z): Prop := ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
(((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((get1 a1 (i1 + i)%Z) = (get1 a2
(i2 + i)%Z))).
Axiom matches_empty : forall (a1:(array char)) (a2:(array char)) (i1:Z)
(i2:Z), ((0%Z <= i1)%Z /\ (i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\
(i2 <= (length a2))%Z) -> (matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
((i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z -> (((get1 a1
(i1 + n)%Z) = (get1 a2 (i2 + n)%Z)) -> (matches a1 i1 a2 i2
(n + 1%Z)%Z)))).
Theorem matches_contradiction_at_first : forall (a1:(array char)) (a2:(array
char)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z -> ((~ ((get1 a1 i1) = (get1 a2
i2))) -> ~ (matches a1 i1 a2 i2 n)).
(* YOU MAY EDIT THE PROOF BELOW *)
unfold get1.
intros (n1,a1) (n2,a2) i1 i2 n Hn.
simpl; intro Heq.
red.
intro Hmatch.
elim Hmatch; simpl; intros (h0,h1) (h2,h3).
absurd (get a1 i1 = get a2 i2); [ assumption | idtac ].
replace i1 with (i1 + 0)%Z.
replace i2 with (i2 + 0)%Z.
apply (h3 0%Z).
omega.
omega.
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.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
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.
Parameter char : Type.
Definition matches(a1:(array char)) (i1:Z) (a2:(array char)) (i2:Z)
(n:Z): Prop := ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
(((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((get1 a1 (i1 + i)%Z) = (get1 a2
(i2 + i)%Z))).
Axiom matches_empty : forall (a1:(array char)) (a2:(array char)) (i1:Z)
(i2:Z), ((0%Z <= i1)%Z /\ (i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\
(i2 <= (length a2))%Z) -> (matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
((i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z -> (((get1 a1
(i1 + n)%Z) = (get1 a2 (i2 + n)%Z)) -> (matches a1 i1 a2 i2
(n + 1%Z)%Z)))).
Axiom matches_contradiction_at_first : forall (a1:(array char)) (a2:(array
char)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z -> ((~ ((get1 a1 i1) = (get1 a2
i2))) -> ~ (matches a1 i1 a2 i2 n)).
Axiom matches_contradiction_at_i : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z -> (((0%Z <= i)%Z /\ (i < n)%Z) ->
((~ ((get1 a1 (i1 + i)%Z) = (get1 a2 (i2 + i)%Z))) -> ~ (matches a1 i1 a2
i2 n))).
Axiom matches_right_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (nqt:Z), (matches a1 i1 a2 i2 n) -> ((nqt < n)%Z ->
(matches a1 i1 a2 i2 nqt)).
Theorem matches_left_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (nqt:Z), (matches a1 (i1 - (n - nqt)%Z)%Z a2
(i2 - (n - nqt)%Z)%Z n) -> ((nqt < n)%Z -> (matches a1 i1 a2 i2 nqt)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros a1 a2 i1 i2 n n' Hmatch Hn.
destruct Hmatch. destruct H0.
red.
split.
omega.
split.
omega.
intros i Hi.
replace (i1 + i)%Z with (i1 - (n - n') + (i + (n - n')))%Z.
replace (i2 + i)%Z with (i2 - (n - n') + (i + (n - n')))%Z.
apply H1.
omega.
omega.
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.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
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.
Parameter char : Type.
Definition matches(a1:(array char)) (i1:Z) (a2:(array char)) (i2:Z)
(n:Z): Prop := ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
(((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((get1 a1 (i1 + i)%Z) = (get1 a2
(i2 + i)%Z))).
Axiom matches_empty : forall (a1:(array char)) (a2:(array char)) (i1:Z)
(i2:Z), ((0%Z <= i1)%Z /\ (i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\
(i2 <= (length a2))%Z) -> (matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
((i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z -> (((get1 a1
(i1 + n)%Z) = (get1 a2 (i2 + n)%Z)) -> (matches a1 i1 a2 i2
(n + 1%Z)%Z)))).
Axiom matches_contradiction_at_first : forall (a1:(array char)) (a2:(array
char)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z -> ((~ ((get1 a1 i1) = (get1 a2
i2))) -> ~ (matches a1 i1 a2 i2 n)).
Axiom matches_contradiction_at_i : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z -> (((0%Z <= i)%Z /\ (i < n)%Z) ->
((~ ((get1 a1 (i1 + i)%Z) = (get1 a2 (i2 + i)%Z))) -> ~ (matches a1 i1 a2
i2 n))).
Axiom matches_right_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (nqt:Z), (matches a1 i1 a2 i2 n) -> ((nqt < n)%Z ->
(matches a1 i1 a2 i2 nqt)).
Axiom matches_left_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (nqt:Z), (matches a1 (i1 - (n - nqt)%Z)%Z a2
(i2 - (n - nqt)%Z)%Z n) -> ((nqt < n)%Z -> (matches a1 i1 a2 i2 nqt)).
Axiom matches_sym : forall (a1:(array char)) (a2:(array char)) (i1:Z) (i2:Z)
(n:Z), (matches a1 i1 a2 i2 n) -> (matches a2 i2 a1 i1 n).
Axiom matches_trans : forall (a1:(array char)) (a2:(array char)) (a3:(array
char)) (i1:Z) (i2:Z) (i3:Z) (n:Z), (matches a1 i1 a2 i2 n) -> ((matches a2
i2 a3 i3 n) -> (matches a1 i1 a3 i3 n)).
Definition is_next(p:(array char)) (j:Z) (n:Z): Prop := ((0%Z <= n)%Z /\
(n < j)%Z) /\ ((matches p (j - n)%Z p 0%Z n) /\ forall (z:Z),
((n < z)%Z /\ (z < j)%Z) -> ~ (matches p (j - z)%Z p 0%Z z)).
Axiom next_iteration : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
(n:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((matches a (i - j)%Z p 0%Z j) -> ((is_next p j
n) -> (matches a (i - n)%Z p 0%Z n)))).
Theorem next_is_maximal : forall (p:(array char)) (a:(array char)) (i:Z)
(j:Z) (n:Z) (k:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((((i - j)%Z < k)%Z /\ (k < (i - n)%Z)%Z) ->
((matches a (i - j)%Z p 0%Z j) -> ((is_next p j n) -> ~ (matches a k p 0%Z
(length p)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros p a.
intros i j n k Hj Hi Hk Hmatch Hnext.
red.
intro Hmax.
elim Hnext; intros h1 (h2, h3).
absurd (matches p (j - (i - k)) p 0 (i - k)).
apply h3; omega.
apply matches_trans with (a2 := a) (i2 := k).
apply matches_sym.
apply matches_left_weakening with (n := j).
replace (k - (j - (i - k)))%Z with (i-j)%Z by ring.
ring_simplify (j - (i - k) - (j - (i - k)))%Z.
assumption.
omega.
apply matches_right_weakening with (n := length p).
assumption.
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.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
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.
Parameter char : Type.
Definition matches(a1:(array char)) (i1:Z) (a2:(array char)) (i2:Z)
(n:Z): Prop := ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
(((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((get1 a1 (i1 + i)%Z) = (get1 a2
(i2 + i)%Z))).
Axiom matches_empty : forall (a1:(array char)) (a2:(array char)) (i1:Z)
(i2:Z), ((0%Z <= i1)%Z /\ (i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\
(i2 <= (length a2))%Z) -> (matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
((i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z -> (((get1 a1
(i1 + n)%Z) = (get1 a2 (i2 + n)%Z)) -> (matches a1 i1 a2 i2
(n + 1%Z)%Z)))).
Axiom matches_contradiction_at_first : forall (a1:(array char)) (a2:(array
char)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z -> ((~ ((get1 a1 i1) = (get1 a2
i2))) -> ~ (matches a1 i1 a2 i2 n)).
Axiom matches_contradiction_at_i : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z -> (((0%Z <= i)%Z /\ (i < n)%Z) ->
((~ ((get1 a1 (i1 + i)%Z) = (get1 a2 (i2 + i)%Z))) -> ~ (matches a1 i1 a2
i2 n))).
Axiom matches_right_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (nqt:Z), (matches a1 i1 a2 i2 n) -> ((nqt < n)%Z ->
(matches a1 i1 a2 i2 nqt)).
Axiom matches_left_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (nqt:Z), (matches a1 (i1 - (n - nqt)%Z)%Z a2
(i2 - (n - nqt)%Z)%Z n) -> ((nqt < n)%Z -> (matches a1 i1 a2 i2 nqt)).
Axiom matches_sym : forall (a1:(array char)) (a2:(array char)) (i1:Z) (i2:Z)
(n:Z), (matches a1 i1 a2 i2 n) -> (matches a2 i2 a1 i1 n).
Axiom matches_trans : forall (a1:(array char)) (a2:(array char)) (a3:(array
char)) (i1:Z) (i2:Z) (i3:Z) (n:Z), (matches a1 i1 a2 i2 n) -> ((matches a2
i2 a3 i3 n) -> (matches a1 i1 a3 i3 n)).
Definition is_next(p:(array char)) (j:Z) (n:Z): Prop := ((0%Z <= n)%Z /\
(n < j)%Z) /\ ((matches p (j - n)%Z p 0%Z n) /\ forall (z:Z),
((n < z)%Z /\ (z < j)%Z) -> ~ (matches p (j - z)%Z p 0%Z z)).
Theorem next_iteration : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
(n:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((matches a (i - j)%Z p 0%Z j) -> ((is_next p j
n) -> (matches a (i - n)%Z p 0%Z n)))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros (np, p) (na, a) i j n Hj Hi Hmatch Hnext.
elim Hnext; intros h (h1, h2).
red; split.
omega.
split.
omega.
intros i0 Hi0.
unfold get1; simpl.
apply trans_equal with (y := get p (j - n + i0)%Z).
elim Hmatch; intros.
replace (i - n + i0)%Z with (i - j + (j - n + i0))%Z.
replace (j - n + i0)%Z with (0 + (j - n + i0))%Z.
apply H0.
omega.
omega.
omega.
elim h1; intros.
apply H0.
omega.
Qed.
(* DO NOT EDIT BELOW *)
This diff is collapsed.
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