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