Module MyLPO

Set Implicit Arguments.
Require Import Setoid.
Require Import MyTactics.
Require Import CoLoR.Term.Varyadic.VSignature.
Require Import CoLoR.Term.Varyadic.VTerm.
Require Import CoLoR.Util.Relation.RelMidex.
Require Import CoLoR.Util.Relation.Preorder.
Require Import CoLoR.RPO.VPrecedence.
Require Import CoLoR.Util.List.LexicographicOrder.
Require Import CoLoR.RPO.VLPO.
Require Import CoLoR.RPO.VRPO_Status.
Require Import CoLoR.RPO.VRPO_Results.

-------------------------------------------------------------------------

Symbols.

In this abstract setting, there are just two symbols: tensor and other.

Proof.

beq_symb_ok.
Qed.

Definition mySig : Signature :=
mkSignature beq_symb_ok.

-------------------------------------------------------------------------

Symbol precedence.

STensor is greater than SOther. This reflects the fact that our reduction rules tend to eliminate a tensor at the root.

Inductive myLeF : mySig -> mySig -> Prop :=
| MyLeFOtherTensor:
    myLeF SOther STensor
| MyLeFEqual:
    forall s,
    myLeF s s.

Local Hint Constructors myLeF.

Module Precedence.

  Definition Sig := mySig.

  Definition leF := myLeF.

  Definition ltF := ltA Sig leF.

  Definition eqF := eqA Sig leF.

  Lemma ltF_wf:
    well_founded ltF.

Proof.

intro s2. constructor; intros s1 [ step1 step2 ]. unfold ltF, ltA, leF, eqA in step1, step2.
dependent destruction step1.

Show that there is nothing below SOther.

clear step2. constructor; intros s3 [ step1 step2 ]. unfold ltF, ltA, leF, eqA in step1, step2.
dependent destruction step1. false; eauto.

Contradiction.

false; eauto.
Qed.

Lemma leF_dec:
rel_dec leF.

Proof.

    unfold leF. intros s1 s2. destruct s1; destruct s2; eauto.
    right. unfold not. inversion 1.
  Qed.

Lemma leF_reflexive:
forall s, leF s s.

Proof.

unfold leF. eauto.
Qed.

Lemma leF_transitive:
forall s1 s2 s3, leF s1 s2 -> leF s2 s3 -> leF s1 s3.

Proof.

unfold leF. introv h1 h2; dependent destruction h1; dependent destruction h2; eauto.
Qed.

Definition leF_preorder : preorder Sig leF :=
Build_preorder Sig leF leF_reflexive leF_transitive.

End Precedence.

-------------------------------------------------------------------------

We now instantiate the modules provided by the CoLoR library, to obtain a definition of, and results about, the lexicographic path ordering.

Module MyLPO := LPO Precedence.

Module MyVLPO := LPO_Model Precedence.

Module VRPO_Results := RPO_Results MyVLPO.

Export VRPO_Results.

Lemma myLPO_wf:
well_founded lt_lpo.

Proof.

apply wf_lt.
Qed.

-------------------------------------------------------------------------

These trivial facts are useful hints for eauto.

Lemma fact1:
SOther <F STensor.

Proof.

unfold ltF, ltA, leF, Preorder.eqA.
split. eauto. intros [ _ h ]. inversion h.
Qed.

Lemma fact2:
forall s,
s =F= s.

Proof.

unfold eqF, Preorder.eqA, leF. eauto.
Qed.

Local Hint Resolve fact1 fact2.

Lemma in2:
  forall (P : term Sig -> Prop),
  forall t1 t2, P t1 -> P t2 ->
  forall t, In t (t1 :: t2 :: nil) -> P t.

Proof.

simpl. intuition idtac; congruence.
Qed.

Lemma in3:
  forall (P : term Sig -> Prop),
  forall t1 t2 t3, P t1 -> P t2 -> P t3 ->
  forall t, In t (t1 :: t2 :: t3 :: nil) -> P t.

Proof.

simpl. intuition idtac; congruence.
Qed.

-------------------------------------------------------------------------

Notation for terms.

Notation other ts :=
  (@Fun Sig SOther ts).

Notation other0 :=
  (other nil).

Notation other1 t1 :=
  (other (t1 :: nil)).

Notation other2 t1 t2 :=
  (other (t1 :: t2 :: nil)).

Notation other3 t1 t2 t3 :=
  (other (t1 :: t2 :: t3 :: nil)).

Notation tensor t1 t2 :=
  (@Fun Sig STensor (t1 :: t2 :: nil)).

-------------------------------------------------------------------------

The lexicographic path ordering contains the sub-term ordering.

Local Hint Constructors lt_lpo.

Local Hint Extern 1 (In _ (_ :: _)) => simpl.

Lemma subterm:
  forall s t ts,
  In t ts ->
  lt_lpo t (@Fun Sig s ts).

Proof.

eauto.
Qed.

Lemma subterm_11:
forall s t1,
lt_lpo t1 (@Fun Sig s (t1 :: nil)).

Proof.

eauto using subterm.
Qed.

Lemma subterm_21:
forall s t1 t2,
lt_lpo t1 (@Fun Sig s (t1 :: t2 :: nil)).

Proof.

eauto using subterm.
Qed.

Lemma subterm_22:
forall s t1 t2,
lt_lpo t2 (@Fun Sig s (t1 :: t2 :: nil)).

Proof.

eauto using subterm.
Qed.

Lemma subterm_31:
forall s t1 t2 t3,
lt_lpo t1 (@Fun Sig s (t1 :: t2 :: t3 :: nil)).

Proof.

eauto using subterm.
Qed.

Lemma subterm_32:
forall s t1 t2 t3,
lt_lpo t2 (@Fun Sig s (t1 :: t2 :: t3 :: nil)).

Proof.

eauto using subterm.
Qed.

Lemma subterm_33:
forall s t1 t2 t3,
lt_lpo t3 (@Fun Sig s (t1 :: t2 :: t3 :: nil)).

Proof.

eauto 6 using subterm.
Qed.

Local Hint Resolve subterm_11 subterm_21 subterm_22 subterm_31 subterm_32 subterm_33.

Hint Resolve subterm_11 subterm_21 subterm_22 subterm_31 subterm_32 subterm_33 : lpo.

-------------------------------------------------------------------------

We now check that the reduction rules that govern tensor are decreasing with respect to this ordering.

Ltac lpo1 :=
  eapply lpo1; [ auto | apply in2 ].

Ltac lpo2 :=
  eapply lpo2; [ auto | apply in2 | idtac ].

Ltac lpo3 :=
  eapply lpo3; intuition eauto 10.

Lemma tensor_simplification_left:
  forall t1 t2 u,
  lt_lpo t1 t2 ->
  lt_lpo (tensor t1 u) (tensor t2 u).

Proof.

  intros. lpo2.
    lpo3.
    eauto.
    apply lex1; auto.
Qed.

Lemma tensor_distribution:
  forall t ts u,
  In t ts ->
  lt_lpo (tensor t u) (tensor (other ts) u).

Proof.

eauto using tensor_simplification_left, subterm.
Qed.

Lemma other_tensor_lt_tensor_other_left:
forall t1 t2 u,
lt_lpo (other2 (tensor t1 u) u) (tensor (other2 t1 t2) u).

Proof.

intros. lpo1; eauto using tensor_distribution.
Qed.

Lemma other_tensor_lt_tensor_other_right:
forall t1 t2 u,
lt_lpo (other2 (tensor t2 u) u) (tensor (other2 t1 t2) u).

Proof.

intros. lpo1; eauto using tensor_distribution.
Qed.

Lemma tensor_arrow_reduction:
forall t1 t2 u,
lt_lpo (other2 (other2 (tensor t1 u) u) (other2 (tensor t2 u) u)) (tensor (other2 t1 t2) u).

Proof.

intros. lpo1; eauto using other_tensor_lt_tensor_other_left, other_tensor_lt_tensor_other_right.
Qed.

Lemma tensor_simultaneous_distribution:
forall ts u,
lt_lpo (other (map (fun t => tensor t u) ts)) (tensor (other ts) u).

Proof.

  intros.
  eapply lpo1; [ auto | idtac ].
  intros ttu h.
  generalize (proj1 (@in_map_iff _ _ (fun t => tensor t u) ts ttu) h); clear h; intros [ t [ ? ? ]]; subst ttu.
  auto using tensor_distribution.
Qed.

Lemma tensor_simultaneous_distribution_arity_0:
forall u,
lt_lpo other0 (tensor other0 u).

Proof.

  intros.
  generalize (tensor_simultaneous_distribution nil); simpl.
  auto.
Qed.

Lemma tensor_simultaneous_distribution_arity_1:
forall t1 u,
lt_lpo (other1 (tensor t1 u)) (tensor (other1 t1) u).

Proof.

  intros.
  generalize (tensor_simultaneous_distribution (t1 :: nil)); simpl.
  auto.
Qed.

Lemma tensor_simultaneous_distribution_arity_2:
forall t1 t2 u,
lt_lpo (other2 (tensor t1 u) (tensor t2 u)) (tensor (other2 t1 t2) u).

Proof.

  intros.
  generalize (tensor_simultaneous_distribution (t1 :: t2 :: nil)); simpl.
  auto.
Qed.

Lemma tensor_selective_distribution_2_2:
forall t1 t2 u,
lt_lpo (other2 t1 (tensor t2 u)) (tensor (other2 t1 t2) u).

Proof.

  intros. lpo1.
    lpo3.
    eauto using tensor_simplification_left.
Qed.

Lemma tensor_selective_distribution_3_2:
forall t1 t2 t3 u,
lt_lpo (other3 t1 (tensor t2 u) t3) (tensor (other3 t1 t2 t3) u).

Proof.

  intros. eapply lpo1; [ auto | apply in3 ].
    lpo3.
    eauto using tensor_simplification_left.
    lpo3.
Qed.

Hint Resolve tensor_simplification_left tensor_arrow_reduction
  tensor_simultaneous_distribution_arity_0
  tensor_simultaneous_distribution_arity_1
  tensor_simultaneous_distribution_arity_2
  tensor_selective_distribution_2_2 tensor_selective_distribution_3_2
  : lpo.