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?

`destruct l2; exact H0`

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

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.

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.

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