The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

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.