The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

(* I think I'm close to finding a way of rewriting with equivalence relations in Set / Type, except [eauto] isn't cooperating. This technique would allow rewriting under quantifiers. It would allow rewriting under lambdas too if an axiom is used. It would only work for terms in the conclusion of a goal. If the term we would want to rewrite isn't in the conclusion of the goal, we'd have to [revert] it first. If it were possible to tell [eauto] to ignore the first n successes, it would be possible to rewrite at the n-th occurrence. It might be necessary to clear the [core] database to avoid interference. I'm not sure if this method would work for a term with a lot of depedent types. *)

Definition iff : Type -> Type -> Type := fun t1 t2 => ((t1 -> t2) * (t2 -> t1))%type.

Definition not : Type -> Type := fun t1 => t1 -> False.

Axiom equivalent : nat -> nat -> Set.

Axiom add : nat -> nat -> nat.

Axiom double : nat -> nat.

Infix "<~>" := iff (at level 95).

Notation "~~" := not.

Infix "~" := equivalent (at level 70).

(* We start our rewrites with this. *)

Axiom iff_forwards : forall t1 t2, (t1 <~> t2) -> t2 -> t1.

Axiom iff_backwards : forall t1 t2, (t1 <~> t2) -> t1 -> t2.

(* This would be our database of compatability theorems. *)

Axiom A1 : forall t1 t2, (t1 <~> t2) -> (~~ t1 <~> ~~ t2).

Axiom A2 : forall t1 t2 t3, (t1 <~> t2) -> ((t1 -> t3) <~> (t2 -> t3)).

Axiom A3 : forall t1 t2 t3, (t1 <~> t2) -> ((t3 -> t1) <~> (t3 -> t2)).

Axiom A4 : forall t1 t2 t3, (t1 <~> t2) -> (t1 + t3 <~> t2 + t3).

Axiom A5 : forall t1 t2 t3, (t1 <~> t2) -> (t3 + t1 <~> t3 + t2).

Axiom A6 : forall t1 t2 t3, (t1 <~> t2) -> (t1 * t3 <~> t2 * t3).

Axiom A7 : forall t1 t2 t3, (t1 <~> t2) -> (t3 * t1 <~> t3 * t2).

Axiom A8 : forall t1 p1 p2, (forall x1, p1 x1 <~> p2 x1) -> ((forall x1 : t1, p1 x1) <~> (forall x1 : t1, p2 x1)).

Axiom A9 : forall t1 p1 p2, (forall x1, p1 x1 <~> p2 x1) -> ({x1 : t1 & p1 x1} <~> {x1 : t1 & p2 x1}).

Axiom A10 : forall n1 n2 n3, n1 ~ n2 -> (n1 ~ n3 <~> n2 ~ n3).

Axiom A11 : forall n1 n2 n3, n1 ~ n2 -> (n3 ~ n1 <~> n3 ~ n2).

Hint Resolve A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 : CompatHints.

(* These are the tactics for rewriting forwards and backwards. *)

Ltac rw_f h1 := refine (iff_forwards _ _ _ _); [solve [eauto 128 using h1 with CompatHints] | lazy beta].

Ltac rw_b h1 := refine (iff_backwards _ _ _ _); [solve [eauto 128 using h1 with CompatHints] | lazy beta].

(* We want to rewrite with this *)

Axiom A12 : forall n1, double n1 ~ add n1 n1.

(* in this.  *)

Goal ~~ ((False -> (False + ((False * (forall x1, {x2 : nat & double x1 ~ x2})) * False)) + False) -> False).

(* This works. *)

refine (iff_forwards _ _ _ _).

eapply A1.

eapply A2.

eapply A3.

eapply A4.

eapply A5.

eapply A6.

eapply A7.

eapply A8.

intro.

eapply A9.

intro.

eapply A10.

eapply A12.

lazy beta.

(* This is supposed to be equivalent, but doesn't work. *)

refine (iff_backwards _ _ _ _).

eauto 128 using A12 with CompatHints.

lazy beta.

(* This too. *)

rw_f A12.

(* It would be possible to build autorewrite databases using the trick that has been posted previously in this mailing list. *)

Tactic Notation "autorw" := rw h1.

Tactic Notation "autorw" := autorw || rw h2.

Tactic Notation "autorw" := autorw || rw h3.