Застрял доказательство леммы с недоказуемыми подцелями - PullRequest
Новая
       68

Застрял доказательство леммы с недоказуемыми подцелями

3 голосов
/ 14 мая 2019

Я пытаюсь доказать лемму, основанную на следующих определениях. 

Section lemma.

Variable A : Type.
Variable P : A -> Prop.

Variable P_dec : forall x, {P x}+{~P x}.

Inductive vector : nat -> Type :=
  | Vnil : vector O
  | Vcons : forall {n}, A -> vector n -> vector (S n).

  Arguments Vcons {_} _ _.

Fixpoint countPV {n: nat} (v : vector n): nat :=
match v with
| Vnil => O
| Vcons x v' => if P_dec x then S (countPV v') else countPV v'
end.

Лемма, которую я пытаюсь доказать, выглядит следующим образом 

Lemma lem: forall (n:nat) (a:A) (v:vector n), 
      S n = countPV (Vcons a v) -> (P a /\ n = countPV v).

Я много чего перепробовал и в данный момент нахожусь на этом этапе. 

Proof.
  intros n a v.
  unfold not in P_dec.
  simpl.
  destruct P_dec.
  - intros.
    split.
    * exact p.
    * apply eq_add_S.
      exact H.
  - intros.
    split.

Контекст на данный момент: 

2 subgoals
A : Type
P : A -> Prop
P_dec : forall x : A, {P x} + {P x -> False}
n : nat
a : A
v : vector n
f : P a -> False
H : S n = countPV v
______________________________________(1/2)
P a
______________________________________(2/2)
n = countPV v

Моя проблема в том, что я застрял с двумя подцелями, которые я не могу доказать, и доступный контекст не кажется полезным. Кто-нибудь может дать мне несколько указателей, чтобы двигаться дальше?

EDIT:

Я доказал лемму, противореча H: 

assert (countPV v <= n).
* apply countNotBiggerThanConstructor.
* omega.
Qed.

где countNotBiggerThanConstructor: 

Lemma countNotBiggerThanConstructor: forall {n : nat} (v: vector n), countPV v <= n.
Proof.
  intros n v.
  induction v.
  - reflexivity.
  - simpl.
    destruct P_dec.
    + apply le_n_S in IHv.
      assumption.
    + apply le_S.
      assumption.
Qed.

1 Ответ

5 голосов
/ 14 мая 2019

Обратите внимание, что H не может быть правдой.Это хорошо, если вы можете доказать Ложь, вы можете доказать что угодно.Так что я бы сделал contradict H дальше (а вам не нужно это последнее split).

В целом ваши доказательства кажутся мне немного беспорядочными.Я предлагаю подумать о том, как вы докажете эту лемму на бумаге, и попытаетесь сделать это в Coq.Я не эксперт в Coq, но я думаю, что это также поможет вам осознать, что вам нужно использовать противоречие в этом случае.но я не могу комментировать с моей 1 репутацией)

...