Stream: Coq users

Topic: inductive application

Andrew (Mar 18 2021 at 00:01):

Hi everyone,
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 slnocut_plusR1 to H to result in a new hypothesis slnocut a b?

Matthieu Sozeau (Mar 18 2021 at 00:29):

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.

Andrew (Mar 18 2021 at 00:40):

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!

Yannick Forster (Mar 18 2021 at 08:42):

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.

Andrew (Mar 18 2021 at 16:41):

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