Search code examples
coqcoq-tactic

COQ Proof Assistant - Apply the hyppothesis

I'm working on a very simple proof assignment in Coqide.
I'm trying to apply hypothesis H2 to my subgoal, but for some reason it's not working. I cannot figure out why; can someone explain why apply H2. command is not applicable.

2 subgoals
A : Type
x : A
l1, l2 : list A
H : Prefix l1 l2
H2 : x :: l2 = (x :: l1) ++ [] -> Prefix (x :: l1) (x :: l2)
______________________________________(1/2)
x :: l2 = (x :: l1) ++ []
______________________________________(2/2)
exists l3 : list A, x :: l2 = (x :: l1) ++ l3
Solution

  • apply H2 has no chance to work because its conclusion is Prefix (x :: l1) (x :: l2) which doesn't look like your goal. The premise of H2 is your goal: x :: l2 = (x :: l1) ++ [] however, which means you can only apply H2 if you manage to solve your goal first… not very useful.