Stream: Equations devs & users

Topic: Noob question about decreasing argument


view this post on Zulip Vincent Siles (Apr 01 2021 at 15:29):

Hi ! I'm testing Equations and have a noob questions:

From Equations Require Import Equations.
From Coq Require Import List.
Import ListNotations.

(* Cannot guess decreasing argument of fix *)
Equations f {A: Type} (a: A) (l:list A)  : list A :=
f a [] := [] ;
f a [x] := [x];
f a (hd :: tl) := hd :: a :: f a tl
.

How to specify the decreasing argument ?

view this post on Zulip Kenji Maillard (Apr 01 2021 at 15:34):

You can add an annotation after the type:

Equations f {A: Type} (a: A) (l:list A)  : list A by struct l :=

view this post on Zulip Kenji Maillard (Apr 01 2021 at 15:35):

But here equations still complains that the recursion does not happen on the right subterm. You can solve it by making more explicit the structure of pattern-matches:

Equations f {A: Type} (a: A) (l:list A)  : list A:=
f a [] := [] ;
f a (hd :: tl) with tl => {
  | [] := [hd] ;
  | _ := hd :: a :: f a tl
}.

view this post on Zulip Vincent Siles (Apr 01 2021 at 15:46):

Perfect, thank you @Kenji Maillard


Last updated: Jan 29 2023 at 16:02 UTC