CODEWITHSUNDEEP
coq
user2809176
user2809176

Reputation: 1275

Coq prove a false list assumption

Given the next theorem.

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.

How to prove the next goal?

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

As I understand an assumption in this case is wrong H : [ ] = rev l2 ++ [n] how to finis the proof? Thanks in advance!

Update. Missing definitions:

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.

I'm trying to prove this theorem:

Theorem rev_injective : forall (l1 l2 : natlist),
    rev l1 = rev l2 -> l1 = l2.

Upvotes: 0

Views: 137

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

As you say you have a false hypothesis in your context, so it doesn't matter what your are trying to prove, it will follow from falsehood. To exploit this you can use the exfalso tactic which replaces your current goal by False. Then you should be able to conclude from rev_injective_helper and H no?

Upvotes: 3

Related Questions