The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 2016-08-09 04:02, Laurent Thery wrote:
>> Anyway an alternative way to automate would be to express the goal only
>> in term of (x mod 3) that can have only 3 values 0 1 2 and check them by
>> computation.

I think that's a great suggestion :) Something like this?

Ltac mod_cases x r m :=
  lazymatch (eval compute in (Z.ltb r m)) with
  | true => (* r < m: destruct *)
    destruct (Z.eq_dec (x mod m) r);
    [ | mod_cases x (Z.succ r) m ]
  | false => (* r ≥ m: absurd case reached *)
    let lt_proof := constr:(ltac:(omega): (m > 0)) in
    pose proof (Z_mod_lt x m lt_proof); omega
  end.

Goal forall x, (x mod 3)%Z =
          (((x mod 3 - - x mod 3) mod 3 - (- x mod 3 - x mod 3) mod 3) mod 
3)%Z.
Proof.
  intros x.
  mod_cases x 0 3;
    repeat match goal with
           | [ H: _ mod _ = 0 |- _ ] => rewrite (Z_mod_zero_opp_full _ _ H)
           | [ H: _ mod _ <> 0 |- _ ] => rewrite (Z_mod_nz_opp_full _ _ H)
           | [ H: _ = _ |- _ ] => rewrite H
           | _ => reflexivity
           end.

> Here is the comlete alternative proof. I think it is nicer.
> ...

Nice. Here's yet another one:

Goal forall x, (x mod 3)%Z =
          (((x mod 3 - - x mod 3) mod 3 - (- x mod 3 - x mod 3) mod 3) mod 
3)%Z.
Proof.
  intros x.
  destruct (Z.eq_dec (x mod 3) 0) as [Heq | ?].

  - rewrite Heq, (Z_mod_zero_opp_full _ _ Heq);
      reflexivity.
  - rewrite Z_mod_nz_opp_full, <- Zminus_mod by assumption.
    match goal with |- _ = ?x mod 3 => ring_simplify x end.
    rewrite <- Zminus_mod_idemp_r, <- Zminus_0_l_reverse, <- 
Zmult_mod_idemp_l, Z.mul_1_l, Zmod_mod;
      reflexivity.
Qed.

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature