I'm stuck on a Coq proof and I'm not sure what to try next. I've got the following development:
Inductive proposition : Prop := | simple (a: proposition) | c_plus (a: proposition) (b: proposition) | c_mult (a: proposition) (b: proposition). Inductive slnocut : proposition -> proposition -> Prop := | slnocut_id : forall (a : proposition), slnocut a a | slnocut_plusR1 : forall (a b c: proposition), slnocut a b -> slnocut a (c_plus b c) | slnocut_plusR2 : forall (a b c: proposition), slnocut a c -> slnocut a (c_plus b c) | slnocut_plusL : forall (a b c : proposition), slnocut a c -> slnocut b c -> slnocut (c_plus a b) c | slnocut_multL1 : forall (a b c : proposition), slnocut a c -> slnocut (c_mult a b) c | slnocut_multL2 : forall (a b c : proposition), slnocut b c -> slnocut (c_mult a b) c | slnocut_multR : forall (a b c : proposition), slnocut a b -> slnocut a c -> slnocut a (c_mult b c). Lemma admis2 : forall (a b c d : proposition), slnocut a (c_plus b c) -> slnocut (c_plus b c) d -> slnocut a d. Proof. intros. apply slnocut_plusR1 in H.
I am stuck on the apply. It says that it can't find an instance for the variable "c", and I've tried using the apply ... with ... with no luck. Might anyone have a hint as to how I can apply
H to result in a new hypothesis
slnocut a b?
You are trying to apply a lemma
forall a' b' c', slnocut a' b' -> slnocut a' (c_plus b' c') to an hypothesis
slnocut a (c_plus b c), so Coq can match the premise
slnocut ?a' ?b' with the hypothesis
slnocut a (c_plus b c), but it does not know what to give for
c. And the result of your application would be that
H : slnocut a (c_plus (cplus b c) ?c') for the
c' you give. Probably not what you're looking for.
Hi Matthieu, thanks for the response. I'm trying to recreate the work in Frank Pfenning's Lecture 1 from OPLSS 2019. I've been able to get to 1:06:24 in the video, but then I get to the problem I shared above and I don't know how to recreate his proof starting at 1:06:24. I know it's outrageous to request this of anyone, but if you have a spare minute to watch the video, here is a link starting at where I'm stuck: https://youtu.be/3aKDnnta9Ck?t=3984. I thought I could use a simple apply to get "proof D" (from the video) as a hypothesis. But no luck so far!
He is doing a proof by induction there, no? I don't think there will be a simple solution via application of a constructor for your lemma, you'll have to prove the full theorem he is proving by a suitable induction, and then in the relevant case it will indeed work by a simple apply of the induction hypothesis.
Hi Yannick, thanks for the guidance. I see what you are saying. I see now that it’s not a good idea to separate this portion of the proof out into a standalone lemma. I will try your suggestion of keeping this within the context of the full theorem. Thanks!
Last updated: Sep 28 2023 at 11:01 UTC