У меня есть схема индукции для вектора, содержащего значение leb (x <= y
),
Definition vector_ind_with_leb : forall (A : Type) (P : forall n y: nat, y <= n -> vector A n -> Prop),
(forall (n : nat) (y : nat) (H : S y <= S n) (a : A) (v : vector A n),
P n y (le_S_n _ _ H) v -> P (S n) (S y) H (insert a v)) ->
(forall (n : nat) (H : 0 <= S n) (a : A) (v : vector A n),
P (S n) 0 H (insert a v)) ->
(forall (y : nat) (H : 0 <= 0), P 0 0 H (empty A)) -> forall (n : nat) (y : nat) (Heq : y <= n) (v : vector A n), P n y Heq v.
have : forall n, 0 <= S n -> 0 <= n.
auto with arith.
move => P' A P H K K'.
refine ( fix Ffix (x : nat) (y : nat) (Heq : y <= x) (x0 : vector _ x) {struct x0} :
P x y Heq x0 := _).
destruct x0.
destruct y.
refine (K n Heq a _).
refine (H n _ Heq a _ (Ffix _ y _ x0)).
have : forall y, y <= 0 -> y = 0.
auto with arith.
move => F'.
set only_0 := F' _ Heq.
destruct y.
refine (K' 0 Heq).
inversion Heq.
Show Proof.
Defined.
Я должен доказать что-то подобное:
Theorem update_vector_correctly : forall {A} n y (x : vector A (S n)) (H : S n >= S y) v, get_value (set_value x (S y) v) (S y) = Some v.
Итак, я получилтри случая.
when (for y and n),
S y <= S n.
0 <= S n.
0 <= 0.
Однако, если вы заметили, например, случай 3 - это абсурд, однажды 0 <> S n
, для всех n
, поэтому я должен помнить, что (S n)
- это число succ.
Когда я использую это: помните (S n).
Я получаю:
H : 0 <= 0
Heqn0 : 0 = S n
Но в первом случае я получаю:
H0 : n1 = S n -> get_value (set_value v0 y0 v) y0 = Some v
Heqn0 : S n1 = S n
, который не является ни ложным, ни истинным случаем. Проблема в том, что моя гипотеза n
, но я должен вернуть P (S n) _ _ (next _ _)
, поэтому отношение равенства не идет "вместе" по индукции, в конце всегда помните, что возникает странная проблема.