Library DemoNat

Demo file on how to use the library: rewrite system for natural numbers

Libraries...

Require Import ssreflect.
Require Import LocConfTac.

Section DemoNat.

Definition of terms

The rewrite system we consider

Section Term.

Hypothesis R : term -> term -> Prop.

Definition Z_r_unit := forall t:term, R (Sum t Zero) t.
Definition Z_r_anni := forall t:term, R (Mult t Zero) Zero.
Definition Succ_Z := R (Succ Zero) One.
Definition O_r_unit := forall t:term, R (Mult t One) t.
Definition O_r_sum := forall t:term, R (Sum t One) (Succ t).
Definition Succ_Sum := forall s t:term, R (Sum s (Succ t)) (Succ (Sum s t)).
Definition Succ_Mult := forall s t:term, R (Mult s (Succ t)) (Sum s (Mult s t)).
Definition Sum_Mult := forall r s t:term, R (Mult r (Sum s t)) (Sum (Mult r s) (Mult r t)).
Definition Sum_cong := forall s t t':term, R t t' -> R (Sum s t) (Sum s t').
Definition Mult_cong := forall s t t':term, R t t' -> R (Mult s t) (Mult s t').
Definition Succ_cong := forall t t':term, R t t' -> R (Succ t) (Succ t').
Definition Sum_com := forall s t:term, R (Sum s t) (Sum t s).
Definition Mult_com := forall s t:term, R (Mult s t) (Mult t s).
Definition Sum_assoc := forall r s t:term, R (Sum (Sum r s) t) (Sum r (Sum s t)).
Definition Mult_assoc := forall r s t:term, R (Mult (Mult r s) t) (Mult r (Mult s t)).

End Term.

Inductive R : term -> term -> Prop :=
| ax1 : Z_r_unit R
| ax2 : Z_r_anni R
| ax3 : O_r_unit R
| ax4 : O_r_sum R
| ax5 : Succ_Sum R
| ax6 : Succ_Mult R
| ax7 : Succ_Z R
| ax8 : Sum_Mult R
| cong1 : Sum_cong R
| cong2 : Mult_cong R
| cong3 : Succ_cong R
| ac1 : Sum_com R
| ac2 : Mult_com R
| ac3 : Sum_assoc R
| ac4 : Mult_assoc R.

Hint Immediate ax1 ax2 ax3 ax4 ax5 ax6 ax7 ax8 ac1 ac2 ac3 ac4.

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 sZ_r_unit : Z_r_unit (Rstar R).
Proof. by startac. Qed.

Lemma sZ_r_anni : Z_r_anni (Rstar R).
Proof. by startac. Qed.

Lemma sSucc_Z : Succ_Z (Rstar R).
Proof. by startac. Qed.

Lemma sO_r_unit : O_r_unit (Rstar R).
Proof. by startac. Qed.

Lemma sO_r_sum : O_r_sum (Rstar R).
Proof. by startac. Qed.

Lemma sSucc_Sum : Succ_Sum (Rstar R).
Proof. by startac. Qed.

Lemma sSucc_Mult : Succ_Mult (Rstar R).
Proof. by startac. Qed.

Lemma sSum_Mult : Sum_Mult (Rstar R).
Proof. by startac. Qed.

Lemma sSum_com : Sum_com (Rstar R).
Proof. by startac. Qed.

Lemma sMult_com : Mult_com (Rstar R).
Proof. by startac. Qed.

Lemma sSum_assoc : Sum_assoc (Rstar R).
Proof. by startac. Qed.

Lemma sMult_assoc : Mult_assoc (Rstar R).
Proof. by startac. Qed.

End Term_prop.

Hint Immediate sZ_r_unit sZ_r_anni sSucc_Z sO_r_unit sO_r_sum sSucc_Sum.
Hint Immediate sSucc_Mult sSum_Mult sSum_com sMult_com sSum_assoc sMult_assoc.

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

Ltac core_step :=
  solve [
      auto
    | apply (Rstar_rcong _ _ cong1); core_step
    | apply (Rstar_rcong _ _ cong2); core_step
    | apply (Rstar_cong _ _ cong3); core_step
    | try_Rstar_in_goal
  ].

Test

Goal forall a, Rstar R (Sum a Zero) a.
by core_step.
Qed.

Goal forall a b, Rstar R (Sum b (Sum a Zero)) (Sum b a).
move => a b.
by core_step.
Qed.

Goal forall a b, Rstar R (Mult b (Sum a Zero)) (Mult b a).
move => a b.
by core_step.
Qed.

Goal Rstar R (Succ (Succ Zero)) (Succ One).
by core_step.
Qed.

Goal forall r s t, R (Mult r (Sum s t)) (Sum (Mult r s) (Mult r t)).
move => r s t.
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
      | Zero => constr : (Zero::nil)
      | One => constr : (One::nil)
      | (Sum ?a ?b) =>
        let x := constr : (Sum b a) in
        let yb := find_ACequiv b in
        let myf := (fun x => constr : (Sum a x)) in
        let y := maplist myf term yb in
          match a with
            | (Sum ?e ?f) =>
              let z := constr : (Sum e (Sum f b)) in
                constr : (x::z::y)
            | _ => constr : (x::y)
          end
      | (Mult ?a ?b) =>
        let x := constr : (Mult b a) in
        let yb := find_ACequiv b in
        let myf := (fun x => constr : (Mult a x)) in
        let y := maplist myf term yb in
          match a with
            | (Mult ?e ?f) =>
              let z := constr : (Mult e (Mult f b)) in
                constr : (x::z::y)
            | _ => constr : (x::y)
          end
      | (Succ ?a) =>
        let xa := find_ACequiv a in
          let myf := (fun x => constr : (Succ x)) in
            maplist myf term xa
      | ?a => constr : (nil (A:=term))
    end.

Some tests

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

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

Goal forall a b c, Rstar R (Mult a (Succ (Sum b c))) (Mult (Succ (Sum 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 (Sum a (Sum b (Sum c d))) (Sum (Sum c a) (Sum d b)).
Proof.
move => a b c d.
try_ACequiv R core_step find_ACequiv 5.
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
      | (Sum ?t Zero) => constr : (LtacYes t)
      | (Mult ?t Zero) => constr : (LtacYes Zero)
      | (Succ Zero) => constr : (LtacYes One)
      | (Mult ?t One) => constr : (LtacYes t)
      | (Sum ?t One) => constr : (LtacYes (Succ t))
      | (Sum ?s (Succ ?t)) => constr : (LtacYes (Succ (Sum s t)))
      | (Mult ?s (Succ ?t)) => constr : (LtacYes (Sum s (Mult s t)))
      | (Mult ?r (Sum ?s ?t)) => constr : (LtacYes (Sum (Mult r s) (Mult r t)))
      | (Sum ?s ?t) =>
              let x := find_nonAC t in
                match x with
                  | LtacYes ?y => constr : (LtacYes (Sum s y))
                  | LtacNo => constr : (LtacNo (term:=A))
                end
      | (Mult ?s ?t) =>
              let x := find_nonAC t in
                match x with
                  | LtacYes ?y => constr : (LtacYes (Mult s y))
                  | LtacNo => constr : (LtacNo (term:=A))
                end
      | (Succ ?t) =>
              let x := find_nonAC t in
                match x with
                  | LtacYes ?y => constr : (LtacYes (Succ y))
                  | LtacNo => constr : (LtacNo (term:=A))
                end
      | ?t => match goal with
                | [ L : Rstar R t t |- _ ] => constr : (LtacNo (term:=A))(* clear trivial loops *)
                | [ L : Rstar R t ?u |- _ ] => constr : (LtacYes u)
                | [ L : R t ?u |- _ ] => constr : (LtacYes u)
              end
      | ?t => constr : (LtacNo (term:=A))
    end.

Goal forall r s, (exists u, Rstar R (Sum (Sum One r) s) u /\ Rstar R (Sum (Sum Zero (s)) (Sum r One)) u).
move => r s.
try_smart_solve R core_step find_nonAC find_ACequiv 2 2.
Qed.

Goal forall r s1 t2,
     exists u : term,
     Rstar R (Sum (Mult r s1) (Mult (Mult r s1) t2)) u /\
     Rstar R (Mult r (Mult s1 (Succ t2))) u.
intros.
try_smart_solve R core_step find_nonAC find_ACequiv 2 2.
Qed.

Goal forall r s t:term, (exists u, Rstar R (Sum (Sum One r) s) u /\ Rstar R (Sum (Sum Zero (s)) (Sum r One)) u).
move => r s t.
try_smart_solve R core_step find_nonAC find_ACequiv 2 2.
Qed.

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

We can now show the local confluence of R almost automatically

Lemma 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 3 3.
elim; try intros...
inversion H0.
rewrite -H3 in H1; inversion H1...
inversion H1.
rewrite -H6 in H3...
elim (H _ _ H3 H6) => v [L1 L2]...
inversion H1.
rewrite <- H5 in *; clear H5.
rewrite <- H3 in *; clear H3.
inversion H2...
rewrite <- H5 in *; clear H5.
rewrite <- H3 in *; clear H3.
inversion H2...
rewrite <- H5 in *; clear H5.
rewrite <- H3 in *; clear H3.
inversion H2...
inversion H7...
inversion H2...
rewrite <- H9 in *...
rewrite <- H9 in *...
rewrite <- H9 in *; clear H9.
inversion H6...
elim (H0 _ _ H6 H10) => v [L1 L2]...
inversion H2...
inversion H2...
rewrite -H6 -H4...
rewrite -H4...
rewrite -H4.
try_various 5 5.
rewrite -H4.
try_various 5 5.
rewrite -H4...
rewrite -H7 in H4.
inversion_clear H4...
inversion H1.
rewrite <- H5 in *; clear H5.
rewrite <- H3 in *; clear H3.
inversion H2...
rewrite <- H5 in *; clear H5.
rewrite <- H3 in *; clear H3.
inversion H2...
rewrite <- H5 in *; clear H5.
inversion H2...
inversion H8...
rewrite <- H5 in *; clear H5.
clear H4 H3 r.
inversion H2...
inversion H6...
inversion H2...
rewrite <- H9 in *...
rewrite <- H9 in *...
rewrite <- H9 in *; clear H9.
inversion H6...
rewrite <- H9 in *; clear H9.
inversion H6...
elim (H0 _ _ H6 H10) => v [L1 L2]...
inversion H2...
rewrite -H4 in H2.
inversion H2...
try_various 0 5.

here we switch the order of things because the final AC-rewrite will be less daunting.

match goal with
| [ |- (exists u:_, Rstar R ?r _ /\ Rstar R ?s _)] =>
have F : exists u:term, Rstar R s u /\ Rstar R r u
end.
try_various 3 5.
elim F => x [L1 L2].
exists x; split; auto.
try_various 5 5.
Qed.

End DemoNat.