We can define `sorted`

on lists of natural numbers using `Fixpoint`

as follows:

```
Fixpoint sorted (l : list nat) : bool :=
match l with
nil => true
| x :: nil => true
| x :: (y :: _) as tl => (x <=? y) && sorted tl
end.
```

I have been trying to use `Equations`

to define the exact same function (with structural recursion), but it seems the `as`

pattern is not accepted and there is no other way around. Any hint? (I finally found a workaround by using well founded recursion with the length, but it feels awkward).

I had exactly the same problem with `as`

recently... and came to the same awkward solution...

This was the function I couldn't Equationize straightforwardly:

```
Inductive T1 : Set :=
| zero
| ocons (alpha : T1) (n : nat) (beta : T1) .
(* short-circuited definition *)
Definition lt (alpha beta : T1) := True.
Fixpoint nf (alpha : T1) : Prop :=
match alpha with
| zero => True
| ocons a n zero => nf a
| ocons a n ((ocons a' n' b') as b) =>
nf a /\ nf b /\ lt a' a
end.
```

What about nested pattern matching? Is the problem that it gives the wrong reduction equations?

or encoding the "foo as b" as "let b := foo in"? (I haven't tried, I'm just triaging)

pretty sure I tried that, can check later today

I finally found the following solution:

```
Equations sorted' (l : list nat) : bool :=
sorted' nil := true;
sorted' (x :: tl) with tl :=
{ | nil := true;
| (y :: _) := (x <=? y) && sorted' tl }.
```

I have yet to check that I obtain the right function (will have to perform a few proofs about the `sorted'`

function).

with `sorted`

defined as follows:

```
Equations sorted (l : list nat) : bool by wf (length l) lt:=
sorted nil := true;
sorted [x] := true;
sorted (x :: y :: tl) := (x <=? y) && sorted (y :: tl).
```

The equivalence between the two functions is straightforward:

```
Lemma sorted_sorted' (l : list nat) : sorted l = sorted' l.
Proof.
funelim (sorted l).
now auto.
now auto.
now rewrite sorted'_equation_2; simpl; rewrite H.
Qed.
```

I hate the `rewrite H`

: `funelim`

chose the name of hypotheses for me. Any hint on how to control that?

Does `apply_funelim`

also introduce the hypotheses?

In the worst case, invoking `f_elim`

by hand might solve the problem, but maybe you will have to be much more explicit.

But it's also possible not to refer to equations:

```
Lemma sorted_sorted' :
forall l, sorted l = sorted' l.
Proof.
intro l.
funelim (sorted l).
- reflexivity.
- reflexivity.
- simp sorted'. f_equal. auto.
Qed.
```

Oh and I forgot to check but `apply_funelim`

does not introduce things indeed:

```
Lemma sorted_sorted' :
forall l, sorted l = sorted' l.
Proof.
intro l.
apply_funelim (sorted l).
- reflexivity.
- reflexivity.
- intros x y l' e. simp sorted'. rewrite e. reflexivity.
Qed.
```

Last updated: May 24 2024 at 23:01 UTC