The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Nov 7, 2011 at 7:26 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Right… So… Short story:

Require Import List.

Record Seq {A:Type} := {
  lst : list A ;
  app : list A -> list A ;
  ok : forall l, app l = lst++l
}.
Implicit Arguments Seq [].

Program Definition append {A:Type} (l r:Seq A) := {|
  lst := app l (lst r);
  app := fun s => app l (app r s)
|}.
Next Obligation.
  intros A [lst1 app1 ok1] [lst2 app2 ok2] s.
  simpl.
  rewrite !ok1, ok2.
  apply app_assoc.
Qed.

 
That's the trick, which is pretty neat I must say. Up to the detail, as Adam noted, that the ok field must be made computationally irrelevant. Which cannot be done in Coq. So… not useful as it is for Coq usage.

That seems similar to an implementation of an assoc_rewrite tactic I came up with recently (the purpose being as a possible example to put into my Coq tutorial, rather than to reinvent the AAC tactics wheel):

Class Associative {X:Type} (op:X->X->X) : Prop :=
| associativity: forall x y z:X,
  op (op x y) z = op x (op y z).

Section assoc_rewrite.

Context `{Associative}.

Infix "*" := op.

Class RightMultOp (x:X) : Type :=
| right_mult: X -> X.

Implicit Arguments right_mult [[RightMultOp]].

Class RightMultValid (x:X) {timesx: RightMultOp x} : Prop :=
| right_mult_valid: forall a:X, timesx a = a * x.

Instance single_right_mult (x:X) : RightMultOp x | 2 :=
fun a:X => a * x.

Program Instance : forall x:X, @RightMultValid x
  (single_right_mult x).
Solve Obligations using reflexivity.

Instance prod_right_mult (x y:X) {timesx:RightMultOp x} :
  RightMultOp (x * y) | 1 :=
fun a:X => timesx a * y.

Instance : forall (x y:X) {timesx:RightMultOp x},
  @RightMultValid x timesx ->
  @RightMultValid (x * y) (@prod_right_mult x y timesx).
Proof.
intros; red; intros.
unfold prod_right_mult.
rewrite H0.
apply associativity.
Qed.

Lemma assoc_rewrite_valid:
  forall {x y:X}
    {timesx:RightMultOp x} `{@RightMultValid x timesx}
    {timesy:RightMultOp y} `{@RightMultValid y timesy},
  x = y -> forall a:X, timesx a = timesy a.
Proof.
intros.
rewrite H0, H1, H2; reflexivity.
Qed.

Example work_out_tactic:
  forall a b c d e:X, b*c*d = e -> a*c*b*c*d*e = a*c*e*e.
Proof.
intros.
pose proof (assoc_rewrite_valid H0).
unfold prod_right_mult, single_right_mult in H1.
rewrite H1.
reflexivity.
Qed.

Ltac assoc_rewrite e :=
  (* first try just rewrite, in case it's at the left *)
  rewrite e ||
  (let H:=fresh in
    pose proof (assoc_rewrite_valid e) as H;
    unfold prod_right_mult, single_right_mult in H;
    rewrite H;
    clear H).

Example repeat_with_tac:
  forall a b c d e:X, b*c*d = e -> a*c*b*c*d*e = a*c*e*e.
Proof.
intros.
assoc_rewrite H0.
reflexivity.
Qed.

Example ex2:
  forall a b c d e:X, b*c = c*d*b -> a*b*c*e = a*c*d*b*e.
Proof.
intros.
assoc_rewrite H0.
reflexivity.
Qed.

End assoc_rewrite.
--
Daniel Schepler