## Stream: Equations devs & users

### Topic: deep pattern matching and recursive guards

#### Yves Bertot (Oct 28 2021 at 08:22):

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).

#### Karl Palmskog (Oct 28 2021 at 08:31):

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.
``````

#### Paolo Giarrusso (Oct 28 2021 at 08:38):

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

#### Paolo Giarrusso (Oct 28 2021 at 08:40):

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

#### Karl Palmskog (Oct 28 2021 at 08:46):

pretty sure I tried that, can check later today

#### Yves Bertot (Oct 28 2021 at 08:52):

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).

#### Yves Bertot (Oct 28 2021 at 09:22):

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?

#### Théo Winterhalter (Oct 28 2021 at 09:40):

Does `apply_funelim` also introduce the hypotheses?

#### Théo Winterhalter (Oct 28 2021 at 09:41):

In the worst case, invoking `f_elim` by hand might solve the problem, but maybe you will have to be much more explicit.

#### Théo Winterhalter (Oct 28 2021 at 09:45):

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.
``````

#### Théo Winterhalter (Oct 28 2021 at 15:55):

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 28 2023 at 18:29 UTC