The Coq mailing list

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

Hi,

  funelim and functional induction are pretty close. Every Equations 
definition comes with its elimination principle and funelim can be called to 
apply it on instantiated calls like Div x (S y) in this example, using 
generalization by equalities for the arguments and function call itself in 
case the return type is dependent. The main difference with Function is that 
the later allows one to write a non-dependent functional (just using Nat.leb 
for the comparison instead of the proof-carrying le_lt_dec) in this case:

Function Div' (x y : nat) {wf lt x} : nat   :=
 match y with
 | 0 => 0
 | _ => if Nat.leb y x then 1 + Div' (x - y) y  else 0
 end.
Proof.
 - intros x y n teq teq0. apply Nat.leb_le in teq0. lia.
 - apply lt_wf.
Qed.

  Of course one can always forget about the dependent types if they’re only 
used to show termination and prove an equivalence with the simply typed 
variant:

Equations? Div (x y : nat) : nat by wf x lt :=
 { Div x 0 := 0 ;
   Div x y with dec (Nat.leb y x) :=
     { | left Hle  := 1 + Div (x - y) y  ;
       | right Hle :=  0 } } .
Proof. subst y. apply Nat.leb_le in Hle.
 lia.
Qed.

Lemma Div_eq (x y : nat) :
  Div x y = match y with 0 => 0 | _ => if Nat.leb y x then 1 + Div (x - y) y 
else 0 end.
Proof.
  funelim (Div x y); try reflexivity.
  now rewrite e.
  now rewrite e0.
Qed.

Best,
-- Matthieu


Le 6 févr. 2019 à 22:18, Jason -Zhong Sheng- Hu 
<fdhzs2010 AT hotmail.com>
 a écrit :

> can't funelim do the same? what's the difference between funelim and 
> functional induction?
> 
> Fact Div_Mod : forall x y,
>   x = S y * Div x (S y) + Mod x (S y).
> Proof.
>   intros. 
>   funelim (Div x (S y));
>     simp Mod; rewrite Heq; clear Heq;
>       simpl; lia.
> Qed.
> 
> Sincerely Yours,
> 
> Jason Hu
> From: 
> coq-club-request AT inria.fr
>  
> <coq-club-request AT inria.fr>
>  on behalf of Pierre Courtieu 
> <pierre.courtieu AT gmail.com>
> Sent: February 6, 2019 3:39 PM
> To: Coq Club
> Subject: Re: [Coq-Club] Equations 1.2beta is out!
>  
> Equations is much more powerfull than Function, especially with
> dependent types, but Function allows to use functional induction,
> which makes proofs easier for students (no need to look for the right
> induction principle + destructs done automatically). Equations should
> allow for that in a future version of Coq.
> 
> Best
> Pierre
> 
> From Coq Require Import Arith Lia.
> Require Import Recdef.
> Goal forall  x y n : nat,  y = S n -> S n <= x
>                                  ->   x - S n < x.
> Proof.
>   intros x y n H H0.
>   lia.
> Qed.
> 
> Function Div (x y : nat) {wf lt x} : nat   :=
>   match y with
>   | 0 => 0
>   | _ => if le_lt_dec y x then 1 + Div (x - y) y  else 0
>   end.
> Proof.
>   - intros x y n teq anonymous teq0.
>     clear teq0. (* lia does not like dependent hyps over its variables *)
>     lia.
>   - apply lt_wf.
> Qed.
> 
> Function Mod (x y : nat) {wf lt x} : nat  :=
>   match y with
>   | 0 => 0
>   | _ => if le_lt_dec y x then Mod (x - y) y else x
>   end.
> Proof.
>   - intros x y n teq anonymous teq0.
>     clear teq0;lia.
>   - apply lt_wf.
> Qed.
> Fact Div_Mod2 x y :
>             x = S y * Div x (S y) + Mod x (S y) .
> Proof.
>   remember (S y) as y'.
>   functional induction Div x y'.
>   - discriminate.
>   - rewrite Mod_equation.
>     rewrite e0 in *|-*.
>     specialize IHn with (1:=eq_refl).
>     clear e0.
>     lia.
> 
>   - rewrite Mod_equation.
>     rewrite e0 in *|-*.
>     clear e0;lia.
> Qed.
> 
> Le mer. 6 févr. 2019 à 16:31, Laurent Thery 
> <Laurent.Thery AT inria.fr>
>  a écrit :
> >
> >
> > Or using the Proof with.
> >
> > Fact Div_Mod x y :
> >   x = S y * Div x (S y) + Mod x (S y).
> > Proof with simp Div Mod in *; try lia.
> >   induction x as [x IH] using lt_wf_ind...
> >   destruct (le_lt_dec _ _) as [H|H]...
> >   assert (x - S y < x) as IH1%IH...
> > Qed.