Adrián García (Jan 11 2022 at 02:22): 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?
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: Sep 23 2023 at 14:01 UTC