Stream: Coq users

Topic: Solving goal with exact


view this post on Zulip Adrián García (Jan 11 2022 at 02:22):

Hello, is it possible to solve this goal by exact IHDC_Proof?

1 subgoal
D, G : LCtx
n : nat
A, B : Formula
H : D  G, (n -: A) s B
IHDC_Proof : [D  G, (n -: A)  B] + nil
______________________________________(1/1)
[D  newHypo G A  B] + nil

I know that the newHypo function should simplify to something as the term in IHDC_Proof, but using exact tactic is not able to know it, is it possible?

view this post on Zulip Michael Soegtrop (Jan 11 2022 at 07:49):

The exact tactic understands unification, so if exact does not work the two terms are not unifiable.

You can see what e.g. Eval cbv in (newHypo G A) evaluates to - maybe replace cbv with simple, hnf or cbn if cbv evaluates too much.

You can also use the change tactic to replace a term with a unifiable term - I use this frequently to see if two terms are indeed unifiable. Say something like change (newHypo G A) with (G, (n -: A)) (I don't know the syntax you use, so I am just guessing).

Finally it might help to switch off notations - sometimes notations give wrong impressions on what the term structure (associativity, ..) is.


Last updated: Feb 01 2023 at 12:30 UTC