The Coq mailing list

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

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.