UniAna.tcfg.Tagleq
Require Import Program.Equality Lia SimplDec.
Require Export ListExtra PreSuffix ListOrder.
Definition Tag := list nat.
Inductive Taglt : Tag -> Tag -> Prop :=
| TagltS (n m : nat) (i : Tag) : n < m -> Taglt (n :: i) (m :: i)
| TagltCons (n m : nat) (i j : Tag) : Taglt i j -> Taglt (n :: i) (m :: j).
Definition Tagle (i j : Tag) : Prop := Taglt i j \/ i = j.
Infix "⊴" := Tagle (at level 70).
Infix "◁" := Taglt (at level 70).
Lemma Tagle_refl (i : Tag)
: i ⊴ i.
Proof.
right;auto.
Qed.
Lemma Taglt_irrefl
: Irreflexive Taglt.
Proof.
unfold Irreflexive, Reflexive, complement.
intros x Hx.
dependent induction Hx.
- lia.
- auto.
Qed.
Lemma Taglt_trans
: Transitive Taglt.
Proof.
intros x y z Hxy Hyz.
revert dependent z.
dependent induction Hxy;intros.
- dependent destruction Hyz.
+ econstructor. lia.
+ econstructor. auto.
- dependent destruction Hyz.
+ econstructor. auto.
+ econstructor. eauto.
Qed.
Hint Resolve Taglt_irrefl Taglt_trans : tagle.
Global Instance Taglt_StrictOrder : StrictOrder Taglt.
Proof.
split; eauto with tagle.
Qed.
Global Instance Tagle_PreOrder : PreOrder Tagle.
Proof.
eapply StrictOrder_PreOrder;eauto.
Qed.
Global Instance Tagle_PartialOrder : PartialOrder eq Tagle.
Proof.
eapply StrictOrder_PartialOrder;eauto.
Qed.
Lemma Taglt_non_nil1 (i : Tag)
: [] ◁ i -> False.
Proof.
intro H. inversion H.
Qed.
Lemma Taglt_non_nil2 (i : Tag)
: i ◁ [] -> False.
Proof.
intro H. inversion H.
Qed.
Hint Immediate Taglt_non_nil1 Taglt_non_nil2 : tagle.
Lemma Taglt_len (i j : Tag)
(Htaglt : i ◁ j)
: | i | = | j |.
Proof.
induction Htaglt;cbn;auto.
Qed.
Lemma Taglt_rcons_le (i j : Tag) (n m : nat)
(Htaglt : i ++ [n] ◁ j ++ [m])
: n <= m.
Proof.
dependent induction Htaglt.
- rewrite cons_rcons' in x0.
rewrite cons_rcons' in x.
eapply app_inj_tail in x0.
eapply app_inj_tail in x.
do 2 destructH. subst n m.
cbn in *.
rinduction i0; cbn in *.
+ lia.
+ rewrite rev_rcons. cbn. reflexivity.
- destruct i0. inversion Htaglt.
destruct j0. inversion Htaglt.
eapply (IHHtaglt (tl i) (tl j));eauto.
+ destruct i;cbn in *;eauto. congruence. inversion x0. eauto.
+ destruct j;cbn in *;eauto. congruence. inversion x. eauto.
Qed.
Lemma Taglt_eq_rcons_lt (i : Tag) (n m : nat)
(Htaglt : i ++ [n] ◁ i ++ [m])
: n < m.
Proof.
induction i;cbn in *.
- inversion Htaglt;subst;auto. inversion H0.
- eapply IHi. inversion Htaglt;subst.
+ lia.
+ auto.
Qed.
Hint Immediate Taglt_irrefl : tagle.
Lemma Taglt_eq_cons_lt (i : Tag) (n m : nat)
(Htaglt : n :: i ◁ m :: i)
: n < m.
Proof.
inversion Htaglt;subst;eauto.
exfalso. eapply Taglt_irrefl; eauto.
Qed.
Lemma Taglt_eq_rcons_Taglt (i j : Tag) (n : nat)
(Htaglt : i ++ [n] ◁ j ++ [n])
: i ◁ j.
Proof.
eapply Taglt_len in Htaglt as Hlen.
do 2 rewrite length_rcons in Hlen. eapply Nat.succ_inj in Hlen.
destruct i;[|revert dependent i; revert dependent n0];induction j;cbn in *;intros.
- exfalso. inversion Htaglt;subst. lia. eauto with tagle.
- lia.
- lia.
- dependent destruction Htaglt.
+ eapply app_inj_tail in x; destruct x;subst.
econstructor;eauto.
+ econstructor.
destruct i,j; cbn in *.
1: exfalso;eapply Taglt_irrefl;eauto.
1,2: lia.
eapply IHj;eauto.
Qed.
Lemma Taglt_le_rcons (n m : nat) (i j : Tag)
(Htaglt : i ◁ j)
(Hle : n <= m)
: i ++ [n] ◁ j ++ [m].
Proof.
induction Htaglt;cbn.
- eapply le_lt_or_eq in Hle. destruct Hle.
+ econstructor;eauto. induction i; cbn; econstructor; eauto.
+ subst. econstructor;eauto.
- econstructor;eauto.
Qed.
Lemma Taglt_lt_rcons (n m : nat) (i j : Tag)
(Hlen : |i| = |j|)
(Hlt : n < m)
: i ++ [n] ◁ j ++ [m].
Proof.
destruct i; intros.
- destruct j; cbn in *.
+ econstructor; eauto.
+ lia.
- revert n0 i Hlen.
induction j; cbn in *; intros.
+ lia.
+ destruct i; cbn in *.
* destruct j; cbn in *; [|lia].
econstructor;econstructor;eauto.
* econstructor.
eapply IHj.
lia.
Qed.
Lemma Taglt_ind_r
(P : Tag -> Tag -> Prop)
(Hbase : forall (n m : nat) (i j : Tag), |i| = |j| -> n < m -> P (i++[n]) (j++[m]))
(Hstep : forall (n : nat) (i j : Tag), Taglt i j -> P i j -> P (i++[n]) (j++[n]))
(i j : Tag)
(Htaglt : Taglt i j)
: P i j.
Proof.
revert dependent j.
rinduction i. 1: exfalso; eauto with tagle.
revert dependent l. revert dependent a.
rinduction j. 1: exfalso; eauto with tagle.
eapply Taglt_len in Htaglt as Hlen.
do 2 rewrite length_rcons in Hlen. eapply Nat.succ_inj in Hlen.
eapply Taglt_rcons_le in Htaglt as Hle.
eapply le_lt_or_eq in Hle.
destruct Hle.
- eapply Hbase;eauto.
- subst a0.
eapply Taglt_eq_rcons_Taglt in Htaglt.
eapply Hstep;eauto.
Qed.
Lemma taglt_tagle_trans (i j k : Tag)
: i ◁ j -> j ⊴ k -> i ◁ k.
Proof.
intros.
destruct H0.
- transitivity j;eauto.
- subst. auto.
Qed.
Lemma tagle_taglt_trans (i j k : Tag)
: i ⊴ j -> j ◁ k -> i ◁ k.
Proof.
intros.
destruct H.
- transitivity j;eauto.
- subst. auto.
Qed.
Lemma le_cons_tagle n1 n2 i
(Hlt : n1 <= n2)
: n1 :: i ⊴ n2 :: i.
Proof.
eapply le_lt_or_eq in Hlt. destruct Hlt.
- econstructor. econstructor. assumption.
- subst. reflexivity.
Qed.
Lemma lt_cons_ntagle n1 n2 i
(Hlt : n2 < n1)
: ~ n1 :: i ⊴ n2 :: i.
Proof.
simpl_dec.
split.
- intro N.
inv N.
+ lia.
+ eapply Taglt_irrefl;eauto.
- intro N. inv N. lia.
Qed.
Lemma taglt_trichotomy i j
(Hlen : |i| = |j|)
: i ◁ j \/ i = j \/ j ◁ i.
Proof.
remember (|i|) as n.
revert i j Heqn Hlen.
induction n;intros.
- destruct i,j;cbn in *;try congruence. right. left. reflexivity.
- destruct i,j;cbn in *;try congruence.
specialize (IHn i j).
exploit IHn.
destruct IHn as [IHn|[IHn|IHn]];[left| |right;right].
+ econstructor;eauto.
+ subst.
specialize (Nat.lt_trichotomy n0 n1) as Hcase.
destruct Hcase as [Hcase|Hcase];[left|right];[|destruct Hcase as [Hcase|Hcase];[left|right]].
* econstructor;eauto.
* subst. reflexivity.
* econstructor;eauto.
+ econstructor;eauto.
Qed.
Lemma tagle_or i j
(Hlen : |i| = |j|)
: i ⊴ j \/ j ⊴ i.
Proof.
eapply taglt_trichotomy in Hlen.
destruct Hlen as [Hlen|[Hlen|Hlen]];[left;left|left;right|right;left];eauto.
Qed.
Lemma Tagle_len: forall [i j : Tag], i ⊴ j -> | i | = | j |.
Proof.
intros. destruct H.
- eapply Taglt_len;eauto.
- subst. reflexivity.
Qed.
Require Export ListExtra PreSuffix ListOrder.
Definition Tag := list nat.
Inductive Taglt : Tag -> Tag -> Prop :=
| TagltS (n m : nat) (i : Tag) : n < m -> Taglt (n :: i) (m :: i)
| TagltCons (n m : nat) (i j : Tag) : Taglt i j -> Taglt (n :: i) (m :: j).
Definition Tagle (i j : Tag) : Prop := Taglt i j \/ i = j.
Infix "⊴" := Tagle (at level 70).
Infix "◁" := Taglt (at level 70).
Lemma Tagle_refl (i : Tag)
: i ⊴ i.
Proof.
right;auto.
Qed.
Lemma Taglt_irrefl
: Irreflexive Taglt.
Proof.
unfold Irreflexive, Reflexive, complement.
intros x Hx.
dependent induction Hx.
- lia.
- auto.
Qed.
Lemma Taglt_trans
: Transitive Taglt.
Proof.
intros x y z Hxy Hyz.
revert dependent z.
dependent induction Hxy;intros.
- dependent destruction Hyz.
+ econstructor. lia.
+ econstructor. auto.
- dependent destruction Hyz.
+ econstructor. auto.
+ econstructor. eauto.
Qed.
Hint Resolve Taglt_irrefl Taglt_trans : tagle.
Global Instance Taglt_StrictOrder : StrictOrder Taglt.
Proof.
split; eauto with tagle.
Qed.
Global Instance Tagle_PreOrder : PreOrder Tagle.
Proof.
eapply StrictOrder_PreOrder;eauto.
Qed.
Global Instance Tagle_PartialOrder : PartialOrder eq Tagle.
Proof.
eapply StrictOrder_PartialOrder;eauto.
Qed.
Lemma Taglt_non_nil1 (i : Tag)
: [] ◁ i -> False.
Proof.
intro H. inversion H.
Qed.
Lemma Taglt_non_nil2 (i : Tag)
: i ◁ [] -> False.
Proof.
intro H. inversion H.
Qed.
Hint Immediate Taglt_non_nil1 Taglt_non_nil2 : tagle.
Lemma Taglt_len (i j : Tag)
(Htaglt : i ◁ j)
: | i | = | j |.
Proof.
induction Htaglt;cbn;auto.
Qed.
Lemma Taglt_rcons_le (i j : Tag) (n m : nat)
(Htaglt : i ++ [n] ◁ j ++ [m])
: n <= m.
Proof.
dependent induction Htaglt.
- rewrite cons_rcons' in x0.
rewrite cons_rcons' in x.
eapply app_inj_tail in x0.
eapply app_inj_tail in x.
do 2 destructH. subst n m.
cbn in *.
rinduction i0; cbn in *.
+ lia.
+ rewrite rev_rcons. cbn. reflexivity.
- destruct i0. inversion Htaglt.
destruct j0. inversion Htaglt.
eapply (IHHtaglt (tl i) (tl j));eauto.
+ destruct i;cbn in *;eauto. congruence. inversion x0. eauto.
+ destruct j;cbn in *;eauto. congruence. inversion x. eauto.
Qed.
Lemma Taglt_eq_rcons_lt (i : Tag) (n m : nat)
(Htaglt : i ++ [n] ◁ i ++ [m])
: n < m.
Proof.
induction i;cbn in *.
- inversion Htaglt;subst;auto. inversion H0.
- eapply IHi. inversion Htaglt;subst.
+ lia.
+ auto.
Qed.
Hint Immediate Taglt_irrefl : tagle.
Lemma Taglt_eq_cons_lt (i : Tag) (n m : nat)
(Htaglt : n :: i ◁ m :: i)
: n < m.
Proof.
inversion Htaglt;subst;eauto.
exfalso. eapply Taglt_irrefl; eauto.
Qed.
Lemma Taglt_eq_rcons_Taglt (i j : Tag) (n : nat)
(Htaglt : i ++ [n] ◁ j ++ [n])
: i ◁ j.
Proof.
eapply Taglt_len in Htaglt as Hlen.
do 2 rewrite length_rcons in Hlen. eapply Nat.succ_inj in Hlen.
destruct i;[|revert dependent i; revert dependent n0];induction j;cbn in *;intros.
- exfalso. inversion Htaglt;subst. lia. eauto with tagle.
- lia.
- lia.
- dependent destruction Htaglt.
+ eapply app_inj_tail in x; destruct x;subst.
econstructor;eauto.
+ econstructor.
destruct i,j; cbn in *.
1: exfalso;eapply Taglt_irrefl;eauto.
1,2: lia.
eapply IHj;eauto.
Qed.
Lemma Taglt_le_rcons (n m : nat) (i j : Tag)
(Htaglt : i ◁ j)
(Hle : n <= m)
: i ++ [n] ◁ j ++ [m].
Proof.
induction Htaglt;cbn.
- eapply le_lt_or_eq in Hle. destruct Hle.
+ econstructor;eauto. induction i; cbn; econstructor; eauto.
+ subst. econstructor;eauto.
- econstructor;eauto.
Qed.
Lemma Taglt_lt_rcons (n m : nat) (i j : Tag)
(Hlen : |i| = |j|)
(Hlt : n < m)
: i ++ [n] ◁ j ++ [m].
Proof.
destruct i; intros.
- destruct j; cbn in *.
+ econstructor; eauto.
+ lia.
- revert n0 i Hlen.
induction j; cbn in *; intros.
+ lia.
+ destruct i; cbn in *.
* destruct j; cbn in *; [|lia].
econstructor;econstructor;eauto.
* econstructor.
eapply IHj.
lia.
Qed.
Lemma Taglt_ind_r
(P : Tag -> Tag -> Prop)
(Hbase : forall (n m : nat) (i j : Tag), |i| = |j| -> n < m -> P (i++[n]) (j++[m]))
(Hstep : forall (n : nat) (i j : Tag), Taglt i j -> P i j -> P (i++[n]) (j++[n]))
(i j : Tag)
(Htaglt : Taglt i j)
: P i j.
Proof.
revert dependent j.
rinduction i. 1: exfalso; eauto with tagle.
revert dependent l. revert dependent a.
rinduction j. 1: exfalso; eauto with tagle.
eapply Taglt_len in Htaglt as Hlen.
do 2 rewrite length_rcons in Hlen. eapply Nat.succ_inj in Hlen.
eapply Taglt_rcons_le in Htaglt as Hle.
eapply le_lt_or_eq in Hle.
destruct Hle.
- eapply Hbase;eauto.
- subst a0.
eapply Taglt_eq_rcons_Taglt in Htaglt.
eapply Hstep;eauto.
Qed.
Lemma taglt_tagle_trans (i j k : Tag)
: i ◁ j -> j ⊴ k -> i ◁ k.
Proof.
intros.
destruct H0.
- transitivity j;eauto.
- subst. auto.
Qed.
Lemma tagle_taglt_trans (i j k : Tag)
: i ⊴ j -> j ◁ k -> i ◁ k.
Proof.
intros.
destruct H.
- transitivity j;eauto.
- subst. auto.
Qed.
Lemma le_cons_tagle n1 n2 i
(Hlt : n1 <= n2)
: n1 :: i ⊴ n2 :: i.
Proof.
eapply le_lt_or_eq in Hlt. destruct Hlt.
- econstructor. econstructor. assumption.
- subst. reflexivity.
Qed.
Lemma lt_cons_ntagle n1 n2 i
(Hlt : n2 < n1)
: ~ n1 :: i ⊴ n2 :: i.
Proof.
simpl_dec.
split.
- intro N.
inv N.
+ lia.
+ eapply Taglt_irrefl;eauto.
- intro N. inv N. lia.
Qed.
Lemma taglt_trichotomy i j
(Hlen : |i| = |j|)
: i ◁ j \/ i = j \/ j ◁ i.
Proof.
remember (|i|) as n.
revert i j Heqn Hlen.
induction n;intros.
- destruct i,j;cbn in *;try congruence. right. left. reflexivity.
- destruct i,j;cbn in *;try congruence.
specialize (IHn i j).
exploit IHn.
destruct IHn as [IHn|[IHn|IHn]];[left| |right;right].
+ econstructor;eauto.
+ subst.
specialize (Nat.lt_trichotomy n0 n1) as Hcase.
destruct Hcase as [Hcase|Hcase];[left|right];[|destruct Hcase as [Hcase|Hcase];[left|right]].
* econstructor;eauto.
* subst. reflexivity.
* econstructor;eauto.
+ econstructor;eauto.
Qed.
Lemma tagle_or i j
(Hlen : |i| = |j|)
: i ⊴ j \/ j ⊴ i.
Proof.
eapply taglt_trichotomy in Hlen.
destruct Hlen as [Hlen|[Hlen|Hlen]];[left;left|left;right|right;left];eauto.
Qed.
Lemma Tagle_len: forall [i j : Tag], i ⊴ j -> | i | = | j |.
Proof.
intros. destruct H.
- eapply Taglt_len;eauto.
- subst. reflexivity.
Qed.