Stream: Coq users

Topic: Triggering reduction under a predicate.

Mycroft92 (Nov 19 2021 at 13:43):

Hi,
In a proof I am attempting, my proof state is:

H: sortedNoDup [a0]
l2: list ident
H0: sortedNoDup (a0 :: l2)
IHl2: sortedNoDup l2 -> sortedNoDup (merge [a0] l2)
============================================
sortedNoDup (a0 :: (fix merge' (c2 : ST) : ST := c2) l2)

As you can see the goal is exactly same as H0 save the reduction of the identity function. Is there a way to force trigger this reduction and allow the proof to go through?

Gaëtan Gilbert (Nov 19 2021 at 13:48):

destruct l2; exact H0
or replace ((fix merge' (c2 : ST) : ST := c2) l2) with l2 by (destruct l2;reflexivity); exact H0

Mycroft92 (Nov 19 2021 at 13:51):

Gaëtan Gilbert said:

destruct l2; exact H0
or replace ((fix merge' (c2 : ST) : ST := c2) l2) with l2 by (destruct l2;reflexivity); exact H0

Thanks. I was hoping cbn would handle this cleanly but I was wrong.

Li-yao (Nov 19 2021 at 14:09):

You need destruct because when you have a fix, its decreasing argument (the only one in this case) must be a constructor (or constructor application), not a variable or function application, for it to reduce.

Mycroft92 (Nov 19 2021 at 14:10):

Li-yao said:

You need destruct because when you have a fix, its decreasing argument (the only one in this case) must be a constructor (or constructor application), not a variable or function application, for it to reduce.

I see. Thanks for the explanation. It makes sense now.

Last updated: Oct 01 2023 at 19:01 UTC