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: Aug 03 2024 at 00:02 UTC