Biorąc pod uwagę następny twierdzenie.

Theorem rev_injective_helper : forall (l : natlist) (n : nat),
    [] = l ++ [n] -> False.
Proof.
  intros l n H.
  unfold app in H.
  induction l. all: inversion H.
Qed.

Jak udowodnić następny cel?

1 subgoal
n : nat
l2 : natlist
H : [ ] = rev l2 ++ [n]
IHl2 : [ ] = rev l2 -> [ ] = l2
______________________________________(1/1)
[ ] = n :: l2

Jak rozumiem założenie w tym przypadku jest nieprawidłowe H : [ ] = rev l2 ++ [n] Jak zakończyć dowód? Z góry dziękuję!

aktualizacja. Brakujące definicje:

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil ⇒ l2
  | h :: t ⇒ h :: (app t l2)
  end.

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil ⇒ nil
  | h :: t ⇒ rev t ++ [h]
  end.

Próbuję udowodnić ten teorety:

Theorem rev_injective : forall (l1 l2 : natlist),
    rev l1 = rev l2 -> l1 = l2.
coq
0
user2809176 22 listopad 2020, 18:02

1 odpowiedź

Najlepsza odpowiedź

Jak mówisz, masz fałszywą hipotezę w kontekście, więc nie ma znaczenia, co próbujesz udowodnić, pójdzie z kłamstwem. Aby to wykorzystać, możesz użyć taktyki exfalso, która zastępuje swój obecny cel przez False. Wtedy powinieneś być w stanie zakończyć z rev_injective_helper i H nie?

3
Théo Winterhalter 22 listopad 2020, 17:38