How to apply a Coq hypothesis of the form A = B -> C = D to a subgoal of the form A = B

0
votes

I'm working on a proof and I'm currently stuck at this. I have a hypothesis which reads: 

T1E : tree1 = EmptyTree -> isEmpty (leftChild (Node tree1 tree2)) = true

I also have a hypothesis: 

H2 : isEmpty (leftChild (Node tree1 tree2)) = true

and my current sub-goal is 

tree1 = EmptyTree

It seems like I should be able to do

rewrite <- T1E

in order to change the subgoal to 

isEmpty (leftChild (Node tree1 tree2)) = true

but when I try that, Coq says

Error: Found no subterm matching "true" in the current goal.

How can I prove my current subgoal using T1E and H2?

1
coq

1 Answers

2
votes

You're probably not going to be able to prove your goal using T1E. Essentially, you're trying to prove A knowing that "if A is true, then B is true`.

However, looking at your context, it seems to me that you should be able to simplify in H2 and get either a contradiction or more information on tree1, which in any case should result in what you want.