Library DemoAlg

Demo file on how to use the library: rewrite system for a module-like system. Strongly inspired by one of the work of Alejandro Díaz Caro (just removed lambda's ).

Libraries
Require Import ssreflect.
Require Import LocConfTac.

Section DemoAlg.

The scalar system

Variable scalar : Set.

Variable Sadd : scalar -> scalar -> scalar.
Variable Smul : scalar -> scalar -> scalar.
Variable S0 : scalar.
Variable S1 : scalar.

Notation "A + B" := (Sadd A B) : scalar_scope.
Notation "A * B" := (Smul A B) : scalar_scope.

Open Scope scalar_scope.

Hypothesis S_0_1_dec : ~ S1 = S0.
Hypothesis S_0_lunit : forall a, S0 + a = a.
Hypothesis S_0_lelim : forall a, S0 * a = S0.
Hypothesis S_1_lunit : forall a, S1 * a = a.
Hypothesis S_rdistrib : forall a b c, a*(b+c) = (a*b)+(a*c).
Hypothesis S_ldistrib : forall a b c, (a+b)*c = (a*c)+(b*c).
Hypothesis S_add_assoc : forall a b c, (a+b)+c = a+(b+c).
Hypothesis S_mul_assoc : forall a b c, (a*b)*c = a*(b*c).
Hypothesis S_add_commut : forall a b, a+b = b+a.
Hypothesis S_mul_commut : forall a b, a*b = b*a.

Close Scope scalar_scope.

Definition of terms

Inductive term : Set :=
| T0 : term
| Tadd : term -> term -> term
| Tmul : scalar -> term -> term
| Tvar : nat -> term
| Tapply : term -> term -> term.

Notation "A +s B" := (Sadd A B) (at level 50) : term_scope.
Notation "A *s B" := (Smul A B) (at level 40) : term_scope.

Notation "A + B" := (Tadd A B) : term_scope.
Notation "A '**' B" := (Tmul A B) (at level 35) : term_scope.
Notation "@ A" := (Tvar A) (at level 10) : term_scope.
Notation "A ; B" := (Tapply A B) (at level 30) : term_scope.

Open Scope term_scope.

The rewrite system we consider

Section Term.

Hypothesis R : term -> term -> Prop.

Elementary rules
Definition R_T0_idem := R (T0 + T0) T0.
Definition R_S0_anni := forall t, R (S0 ** t) T0.
Definition R_S1_unit := forall t, R (S1 ** t) t.
Definition R_T0_anni := forall a, R (a ** T0) T0.
Definition R_mul_abs := forall a b t, R (a ** (b ** t)) ((a *s b) ** t).
Definition R_ma_dist := forall a s t, R (a ** (s + t)) (a ** s + a ** t).
Assoc. and commut. of addition
Definition R_add_com := forall s t, R (s + t) (t + s).
Definition R_add_rassoc := forall r s t, R ((r + s) + t) (r + (s + t)).
Definition R_add_lassoc := forall r s t, R (r + (s + t)) ((r + s) + t).
Congruence
Definition R_cong_mul := forall a s t, R s t -> R (a**s) (a**t).
Definition R_cong_ladd := forall u s t, R s t -> R (s+u) (t+u).
Definition R_cong_radd := forall u s t, R s t -> R (u+ s) (u+t).
Definition R_cong_lapp := forall u s t, R s t -> R (s;u) (t;u).
Definition R_cong_rapp := forall u s t, R s t -> R (u;s) (u;t).
Linearity of application
Definition R_add_app_ldist := forall r s t, R ((r + s);t) (r;t + s;t).
Definition R_mul_app_ldist := forall a r s, R ((a**r);s) (a**(r;s)).
Definition R_T0_app_ldist := forall s, R (T0;s) T0.
Definition R_add_app_rdist := forall r s t, R (t;(r + s)) (t;r + t;s).
Definition R_mul_app_rdist := forall a r s, R (s;(a**r)) (a**(s;r)).
Definition R_T0_app_rdist := forall s, R (s;T0) T0.

End Term.

Inductive R : term -> term -> Prop :=
| ax1 :R_T0_idem R
| ax2 :R_S0_anni R
| ax3 :R_S1_unit R
| ax4 :R_T0_anni R
| ax5 :R_mul_abs R
| ax6 :R_ma_dist R

| ax10 :R_add_com R
| ax11 :R_add_rassoc R
| ax12 :R_add_lassoc R

| ax13 :R_cong_mul R
| ax14 :R_cong_ladd R
| ax15 :R_cong_radd R
| ax16 :R_cong_lapp R
| ax17 :R_cong_rapp R

| ax18 :R_add_app_ldist R
| ax19 :R_mul_app_ldist R
| ax20 :R_T0_app_ldist R
| ax21 :R_add_app_rdist R
| ax22 :R_mul_app_rdist R
| ax23 :R_T0_app_rdist R.

Hint Immediate ax1 ax2 ax3 ax4 ax5 ax6 ax10 ax11 ax12 ax18 ax19 ax20 ax21 ax22 ax23.

Some properties to be able to automate the reduction process

Section Term_prop.

Ltac startac := match goal with | [ |- ?A _ ] => unfold A end; intros;
  match goal with | [ |- Rstar _ _ ?A ] => apply (Rcons _ _ _ A) end; auto.

Lemma Sax1 : R_T0_idem (Rstar R).
Proof. by startac. Qed.

Lemma Sax2 : R_S0_anni (Rstar R).
Proof. by startac. Qed.

Lemma Sax3 : R_S1_unit (Rstar R).
Proof. by startac. Qed.

Lemma Sax4 : R_T0_anni (Rstar R).
Proof. by startac. Qed.

Lemma Sax5 : R_mul_abs (Rstar R).
Proof. by startac. Qed.

Lemma Sax6 : R_ma_dist (Rstar R).
Proof. by startac. Qed.

Lemma Sax10 : R_add_com (Rstar R).
Proof. by startac. Qed.

Lemma Sax11 : R_add_rassoc (Rstar R).
Proof. by startac. Qed.

Lemma Sax12 : R_add_lassoc (Rstar R).
Proof. by startac. Qed.

Lemma Sax18 : R_add_app_ldist (Rstar R).
Proof. by startac. Qed.

Lemma Sax19 : R_mul_app_ldist (Rstar R).
Proof. by startac. Qed.

Lemma Sax20 : R_T0_app_ldist (Rstar R).
Proof. by startac. Qed.

Lemma Sax21 : R_add_app_rdist (Rstar R).
Proof. by startac. Qed.

Lemma Sax22 : R_mul_app_rdist (Rstar R).
Proof. by startac. Qed.

Lemma Sax23 : R_T0_app_rdist (Rstar R).
Proof. by startac. Qed.

End Term_prop.

Hint Immediate Sax1 Sax2 Sax3 Sax4 Sax5 Sax6 Sax10 Sax11 Sax12 Sax18 Sax19 Sax20 Sax21 Sax22 Sax23.

Tactic to prove automatically that Rstar R a b for trivial cases

Ltac core_step :=
  solve [
      auto
    | apply (Rstar_cong _ _ (ax13 _)); core_step
    | apply (Rstar_lcong _ _ ax14); core_step
    | apply (Rstar_rcong _ _ ax15); core_step
    | apply (Rstar_lcong _ _ ax16); core_step
    | apply (Rstar_rcong _ _ ax17); core_step
    | try_Rstar_in_goal
  ].

Test

Goal forall a, Rstar R (S0 ** a) T0.
by core_step.
Qed.

Goal forall a b, Rstar R (b**(T0;a)) (b**T0).
move => a b.
by core_step.
Qed.

Given x, find the possible AC-conversions and construct a list of empty trees with these terms as roots.
Ltac find_ACequiv r :=
    match r with
      | T0 => constr : (T0::nil)
      | (Tvar ?a) => constr : ((Tvar a)::nil)
      | (Tadd ?a ?b) =>
        let x := constr : (Tadd b a) in
        let yb := find_ACequiv b in
        let myf := (fun x => constr : (Tadd a x)) in
        let y := maplist myf term yb in
          match a with
            | (Tadd ?e ?f) =>
              let z := constr : (Tadd e (Tadd f b)) in
                constr : (x::z::y)
            | _ => constr : (x::y)
          end
      | (Tapply ?a ?b) =>
        let yb := find_ACequiv b in
        let myf := (fun x => constr : (Tapply a x)) in
        let y := maplist myf term yb in
        let y'a := find_ACequiv a in
        let myg := (fun x => constr : (Tapply x b)) in
        let y' := maplist myg term y'a in
        applist y y'
      | (Tmul ?a ?b) =>
        let yb := find_ACequiv b in
        let myg := (fun x => constr : (Tmul a x)) in
        maplist myg term yb
      | ?a => constr : (nil (A:=term))
    end.

Some tests

Goal forall a b c, Rstar R (a + (b + c)) (a + (c + b)).
Proof.
move => a b c.
try_ACequiv R core_step find_ACequiv 1.
Show Proof.
Qed.

Goal forall a b c, Rstar R ((a + (b + c));(a + (b + c))) ((a + (c + b));((c + b)+a)).
Proof.
move => A B C.
try_ACequiv R core_step find_ACequiv 2.
Show Proof.
Qed.

Goal forall a b c d, Rstar R (a + (b**(c+d))) (((b**(d+c))) + a).
Proof.
move => A b C D.
try_ACequiv R core_step find_ACequiv 1.
Show Proof.
Qed.

Tactic that gives a potential next element using non-AC rewrites. The idea is that since the RW system is locally confluent (and normalizing), regardless of the term we choose it should not matter.

Ltac find_nonAC a :=
  let A := typeof a in
    match a with
      | (T0 + T0) => constr : (LtacYes T0)
      | (S0 ** _) => constr : (LtacYes T0)
      | (S1 ** ?t) => constr : (LtacYes t)
      | (_ ** T0) => constr : (LtacYes T0)
      | (?a ** (?b ** ?x)) => constr : (LtacYes ((Smul a b) ** x))
      | (?a ** (?s + ?t)) => constr : (LtacYes ((a ** s) + (a ** t)))
      | (?u;(?s + ?t)) => constr : (LtacYes ((u;s) + (u;t)))
      | ((?s + ?t);?u) => constr : (LtacYes ((s;u) + (t;u)))
      | (?u;(?a ** ?t)) => constr : (LtacYes (a ** (u;t)))
      | ((?a ** ?t);?u) => constr : (LtacYes (a ** (t;u)))
      | (_;T0) => constr : (LtacYes (T0))
      | (T0;_) => constr : (LtacYes (T0))
      | (Tadd ?s ?t) =>
              let x := find_nonAC t in
                match x with
                  | LtacYes ?y => constr : (LtacYes (Tadd s y))
                end
      | (Tadd ?s ?t) =>
              let x := find_nonAC s in
                match x with
                  | LtacYes ?y => constr : (LtacYes (Tadd y t))
                end
      | (Tapply ?s ?t) =>
              let x := find_nonAC t in
                match x with
                  | LtacYes ?y => constr : (LtacYes (Tapply s y))
                end
      | (Tapply ?s ?t) =>
              let x := find_nonAC s in
                match x with
                  | LtacYes ?y => constr : (LtacYes (Tapply y t))
                end
      | (Tmul ?a ?t) =>
              let x := find_nonAC t in
                match x with
                  | LtacYes ?y => constr : (LtacYes (Tmul a y))
                end
      | ?t => match goal with
                | [ L : Rstar R t t |- _ ] =>
                  move : L; let y := find_nonAC a in
                    move => L; constr : y
                | [ L : Rstar R t ?u |- _ ] => constr : (LtacYes u)
                | [ L : R t ?u |- _ ] => constr : (LtacYes u)
              end
      | ?t => constr : (LtacNo (term:=A))
    end.

Some tests.

Goal forall a b,
  Rstar R a (S0 ** b) ->
  Rstar R a T0.
move => a b H.
repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv 3 H).
auto.
Qed.

Goal forall a b c,
  Rstar R a ((S0 ** b);(c)) ->
  Rstar R a T0.
move => a b c H.
repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv 3 H).
auto.
Qed.

Goal forall a x u v w,
  Rstar R x (u ; (a ** (v + w))) ->
  Rstar R x ((a ** (u;v)) + (a ** (u;w))).
move => a x u v w H.
repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv 3 H).
auto.
Qed.

Goal forall a b x u v,
  Rstar R x ((a ** u); (S1**(b ** v))) ->
  Rstar R x ((Smul b a) ** (u;v)).
move => a b x u v H.
repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv 3 H).
auto.
Qed.

Goal forall x y, Rstar R x (T0 + (y + T0)) -> Rstar R x (y + T0).
move => x y H.
repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv 4 H).
auto.
Qed.

make it a bit more smart

Ltac try_various d1 d2 :=
  try solve [
    match goal with
      | [ H : R T0 _ |- _ ] => inversion H
    end
    |
      try_smart_solve R core_step find_nonAC find_ACequiv d1 d2
].

Define a shortcut for go_as_far_as_possible.

Ltac go_forward :=
  go_as_far_as_possible R core_step find_nonAC find_ACequiv.

We can now show the local confluence of R almost automatically

Theorem R_local_confluence : forall r s t:term,
  (R r s) -> (R r t) -> exists u:term, (Rstar R s u) /\ (Rstar R t u).
Proof with (try_various 5 5).
elim.
intros...
move => s IHs t IHt u v H K.
inversion H...
rewrite <- H1 in *; clear H1.
rewrite <- H2 in *; clear H2.
inversion K...
rewrite <- H1 in *; inversion K...
try_various 1 8.
rewrite <- H2 in *; inversion K...
inversion K...
rewrite <- H5 in H3...
rewrite <- H5 in *...
elim (IHs _ _ H3 H7) => x [L1 L2]...
inversion K...
rewrite <- H6 in H3...
rewrite <- H6 in H3...
elim (IHt _ _ H3 H7) => x [L1 L2]...
move => a r IHr s t H K.
inversion H...
rewrite <- H1 in *.
inversion K...
rewrite S_0_lelim...
rewrite <- H1 in *.
inversion K...
symmetry in H4.
elim (S_0_1_dec H4).
rewrite -H0 -H3...
rewrite -H0 -H5...
rewrite S_1_lunit.
rewrite H5 H0...
rewrite -H0 -H5...
rewrite -H0...
rewrite <- H2 in *.
inversion K...
rewrite <- H2 in *.
inversion K...
rewrite <- H3 in *.
rewrite <- H4 in *.
rewrite S_0_lelim...
rewrite <- H4 in *.
rewrite S_1_lunit...
inversion H6...
rewrite -H8 S_mul_commut S_0_lelim...
rewrite -H8 S_mul_commut S_1_lunit...
go_forward.
rewrite S_mul_assoc...
rewrite <- H2 in *.
inversion K...
rewrite -H4...
rewrite -H4...
inversion H6...
inversion K...
rewrite -H5...
rewrite <- H5 in *; clear H5.
rewrite <- H4 in *; clear H4.
auto...
rewrite <- H6 in *; clear H6.
rewrite <- H4 in *; clear H4.
rewrite <- H1 in *; clear H1.
inversion H...
rewrite <- H6 in *; clear H6.
rewrite <- H4 in *; clear H4.
rewrite <- H1 in *; clear H1.
inversion H3...
rewrite -H4 -S_mul_commut S_0_lelim...
rewrite -H4 S_mul_commut S_1_lunit...
go_forward.
rewrite S_mul_assoc...
rewrite <- H6 in *.
inversion H3...
elim (IHr _ _ H3 H7) => x [L1 L2]...
move => ? ? ? H ?.
inversion H.
move => r IHr s IHs t u H K.
inversion H.
inversion K...
elim (IHr _ _ H3 H7) => x [L1 L2]...
rewrite <- H5 in *.
inversion H3...
rewrite <- H5 in *.
inversion H3...
rewrite -H8...
rewrite -H8...
rewrite -H5 in H3; inversion H3.
inversion K...
elim (IHs _ _ H3 H7) => x [L1 L2]...
rewrite <- H6 in *; inversion H3...
rewrite <- H6 in *; inversion H3...
rewrite -H8...
rewrite -H8...
rewrite -H6 in H3; inversion H3.
rewrite <- H1 in *.
inversion K...
inversion H6...
try_various 2 8.
rewrite <- H1 in *.
inversion K...
inversion H6...
rewrite -H8...
rewrite -H8...
go_forward.
rewrite S_mul_commut...
rewrite -H1 in K; inversion K...
rewrite <- H2 in *.
inversion K.
auto...
inversion H6...
try_various 2 8.
auto...
auto...
rewrite <- H4 in *.
inversion K...
rewrite <- H2 in *.
inversion K...
inversion H6...
rewrite -H8...
rewrite -H8...
go_forward.
rewrite S_mul_commut...
rewrite <- H2 in *; inversion K...
Qed.

End DemoAlg.