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.
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).
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).
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).
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.
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.
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.