The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Yes sorry funelim does the same already.

Le jeu. 7 févr. 2019 à 09:00, Matthieu Sozeau
<matthieu.sozeau AT inria.fr>
 a écrit :
>The main difference with Function is that the later allows one to write a 
>non-dependent functional ...

For the record I think you meant "non-dependent functional equation".

Equations is meant to subsume strictly Function at some point. It
could even become its backend (Function being just an "ML-ish" wrapper
around the more powerful "agda-ish" Equations).

The other noticeable difference still around is that Function tries to
build elimination principles that follow the originally written
pattern-matching.

Try for instance:

Function f (n:nat): nat :=
  match n with
  | 10 => 0
  | n => n + 1
  end.

Goal forall n, f n <> 10 -> f n = n + 1.
  intros n.
  functional induction (f n).
  (* 2 cases: 10 and not 10 *)
and:


Equations f (n:nat) : nat :=
  { f 10 := 0;
    f x  := x + 1}.

Goal forall n, n <> 10 -> f n = n + 1.
Proof.
  intros n.
  funelim (f n).
 (* 11 cases: 0 1 ... 10 , more than 10 *)

Note however that this "compaction" of the elimination principle
cannot be done in general in a dependently typed pattern matching.

Best,
Pierre