The Coq mailing list

[<rpgcbaptista AT gmail.com>]

Hello club,

I don't have much experience writing tactics, so I was wondering why mine
gives an error. It's a tactic for rewriting with equivalences. I don't want to
use the Setoid module because the theorems it uses are opaque. My tactic
fails, but when I use its body directly, I don't have any problems. It's at
the end of this code:

Axiom PosInt : Set.
Axiom N : Set.

Notation "'Z+'" := PosInt (at level 0, no associativity).

Axiom one : Z+.
Axiom add : Z+ -> Z+ -> Z+.
Axiom zer : N.
Axiom pos : Z+ -> N.
Axiom succ : N -> Z+.
Axiom div : Z+ -> Z+ -> N.
Axiom mod : Z+ -> Z+ -> N.

Notation "1" := one (at level 0, no associativity).
Notation "i1 + i2" := (add i1 i2) (at level 50, left associativity).
Notation "0" := zer (at level 0, no associativity).
Notation "+ i1" := (pos i1) (at level 35, right associativity).
Notation "'s' n1" := (succ n1) (at level 35, right associativity).
Notation "i1 / i2" := (div i1 i2) (at level 40, left associativity).
Notation "i1 'mod' i2" := (mod i1 i2) (at level 40, left associativity).

Axiom add_comm : forall i1 i2, i1 + i2 = i2 + i1.
Axiom one_add : forall i1 i2, 1 = i1 + i2 -> False.
Axiom zer_pos : forall i1, 0 = + i1 -> False.
Axiom div_eq_1 : forall i1, i1 / i1 = + 1.
Axiom div_eq_2 : forall i1 i2, i1 / (i1 + i2) = 0.
Axiom div_eq_3 : forall i1 i2, (i1 + i2) / i2 = + (s (i1 / i2)).
Axiom mod_eq_1 : forall i1, i1 mod i1 = 0.
Axiom mod_eq_2 : forall i1 i2, i1 mod (i1 + i2) = + i1.
Axiom mod_eq_3 : forall i1 i2, (i1 + i2) mod i2 = i1 mod i2.

Axiom ind_1 : forall P1 : Z+ -> Type,
  P1 1 ->
  (forall i1, P1 (i1 + 1)) ->
  forall i1, P1 i1.

Axiom ind_2 : forall P1 : Z+ -> Type,
  P1 1 ->
  (forall i1, P1 (i1 + i1)) ->
  (forall i1, P1 (i1 + i1 + 1)) ->
  forall i1, P1 i1.

Axiom ind_3 : forall P1 : Z+ -> Z+ -> Type,
  (forall i1, P1 i1 i1) ->
  (forall i1 i2, P1 i1 (i1 + i2)) ->
  (forall i1 i2, P1 (i1 + i2) i2) ->
  forall i1 i2, P1 i1 i2.

Axiom ind_4 : forall P1 : Z+ -> Type,
  (forall i1, (forall i2 i3, i1 = i2 + i3 -> P1 i2) -> P1 i1) ->
  forall i1, P1 i1.

Axiom OJQZ : forall {i1}, 0 = + i1 <-> False.
Axiom EKLO : forall i1 i2, i1 / (i2 + i1) = 0.
Axiom ZHVB : forall i1 i2, i1 mod (i2 + i1) = + i1.

Ltac rw_aux theor := progress repeat
  match goal with
  | [H1 : _ |- _] => progress (
    apply (proj1 theor) in H1 ||
    (try apply eq_sym in H1; apply (proj1 theor) in H1; try apply eq_sym in
H1))
  | [|- _] => progress (
    apply (proj2 theor) ||
    (try apply eq_sym; apply (proj2 theor); try apply eq_sym))
  end.

Ltac rw := progress repeat (
  rewrite div_eq_1 in * ||
  rewrite div_eq_2 in * ||
  rewrite div_eq_3 in * ||
  rewrite mod_eq_1 in * ||
  rewrite mod_eq_2 in * ||
  rewrite mod_eq_3 in * ||
  rw_aux OJQZ ||
  rewrite EKLO in * ||
  rewrite ZHVB in *).

Theorem bin_div_mod_eq_5 : forall i1 i2, i1 / i2 = 0 -> i1 mod i2 = 0 ->
  (i1 + i1) / i2 = 0.
Proof.
intros i1.
remember (i1 + i1) as i3 in |-.
revert i1 Heqi3.
induction i3 as [i3 H1] using ind_4.
intros i1 H2 i2 H3 H4.
functional induction (i3 / i2) using ind_3 as [i3 | i3 i2 | i3 i2].

  rw.

  rw_aux OJQZ. (* <- This fails *)

  progress repeat
  match goal with
  | [H1 : _ |- _] => progress (
    apply (proj1 OJQZ) in H1 ||
    (apply eq_sym in H1; apply (proj1 OJQZ) in H1; try apply eq_sym in H1))
  | [|- _] => progress (
    apply (proj2 OJQZ) ||
    (apply eq_sym; apply (proj2 OJQZ); try apply eq_sym))
  end. (* <- This works even though it's just the body of rw_aux *)

Thank you for your time.