The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

> Le 11 févr. 2019 à 14:32, Pierre Courtieu 
> <pierre.courtieu AT gmail.com>
>  a écrit :
> 
> 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 ».

Hi,

I was thinking of the Function implementation, which gives you the functional 
equation.
If you write the Equations version using only Nat.leb then you won’t get 
enough logical 
information to justify the recursive calls. Hence the need for dec / 
sumbool_of_bool.

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

Indeed, that a good point. One can use views to encode this using dependent
pattern-matching, e.g.:

(* Discriminate the 10 case *)
Equations discr_10 (x : nat) : Prop :=
  discr_10 10 := False;
  discr_10 x := True.

Module View.
Inductive view_discr_10 : nat -> Set :=
| view_discr_10_10 : view_discr_10 10
| view_discr_10_other c : discr_10 c -> view_discr_10 c.

(** This view is obviously inhabited for any element in [nat]. *)
Equations discr_10_view c : view_discr_10 c :=
discr_10_view 10 := view_discr_10_10;
discr_10_view c := view_discr_10_other c I.

Equations f (n:nat) : nat :=
f n with discr_10_view n :=
f ?(10) view_discr_10_10 := 0;
f ?(n) (view_discr_10_other n Hn) := n + 1.

Goal forall n, n <> 10 -> f n = n + 1.
  intros n; apply f_elim.
 (* 2 cases: 10 and not 10 *)
  all:simpl; congruence.
Qed.

End View.

Where view_discr_10 encodes the view of nat as 10 + {N \ 10}.
This is a bit heavy but explicit.
Another option is to replicate what Function is doing, e.g:

Equations f (n:nat) : nat by struct n (* annotation due to an unrelated bug 
*) :=
{ f 10 := 0;
  f x  := brx x (I : discr_10 x) }
(* brx is type-checked only once, and can use the hypothesis *)
where brx (x : nat) (H : discr_10 x) : nat :=
      brx x H := x + 1.

(* We can automatically remove the 11 cases of the second clause. *)
Lemma f_elim' : forall (P : nat -> nat -> Prop),
    P 10 0 ->
    (forall (x : nat) (H : discr_10 x), P x (x + 1)) ->
    (forall n : nat, P n (f n)).
Proof.
  intros. apply (f_elim P (fun x H r => P x r)); auto.
Qed.

Goal forall n, n <> 10 -> f n = n + 1.
  intros n; apply f_elim'; simpl; congruence.
 (* 2 cases: 10 and not 10 *)
Qed.

Automating one or the other is certainly possible but it’s not immediately 
clear to me how it would integrate with the syntax of programs. In principle
I think any of the two options could deal with dependencies: the discriminator
would just get more involved.

Best,
— Matthieu