Coq: Как правильно запомнить зависимые значения, не испортив гипотезу индукции? - PullRequest
Новая
       85

Coq: Как правильно запомнить зависимые значения, не испортив гипотезу индукции?

0 голосов
/ 12 октября 2019

У меня есть схема индукции для вектора, содержащего значение 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 _ _), поэтому отношение равенства не идет "вместе" по индукции, в конце всегда помните, что возникает странная проблема.

1 Ответ

0 голосов
/ 29 октября 2019

Решением является generalize dependent n между remember и induction. Проблема, с которой вы столкнулись, заключается в следующем:

У вас есть это n1 = S n для данного n, и вы хотите индуцировать более n1 (фактически по вектору, но это не такдело для наших целей). Сначала Coq обобщает вашу цель на все, что зависит от n1 (включая доказательство того, что n1 = S n). Но это неверная гипотеза индукции;Вы не пытаетесь доказать свое утверждение по индукции, только когда n1 является преемником этого конкретного n. Вместо этого вы хотите доказать свое утверждение, когда n1 является преемником any n, и, следовательно, вы должны обобщить значение n перед выполнением индукции.

В качестве альтернативы, вВ этом случае вы могли бы сначала доказать, что S n <> 0, и тогда вам не нужно ничего remember, так как в вашем третьем случае уже есть абсурдная гипотеза.

...