Require Import HFS.Tree.
Implicit Types s t u v : tree.
Inductive equiv : tree -> tree -> Prop:=
| equivCancel s t : equiv (s@s@t) (s@t)
| equivSwap s t u : equiv (s@t@u) (t@s@u)
| EquivCongruent s s' t t' : equiv s s' -> equiv t t' -> equiv (s@t) (s'@t')
| EquivRefl s : equiv s s
| EquivSymm s t : equiv s t -> equiv t s
| EquivTrans s t u : equiv s t -> equiv t u -> equiv s u.
Notation "s '==' t" := (equiv s t) (at level 70). (* s ≈ t *)
Notation "s 'elt' t" := (equiv (s@t) t) (at level 70). (* s ∈ t *)
Instance equiv_Equivalence :
Equivalence equiv.
Proof.
constructor; cbv; eauto using equiv.
Qed.
Instance equiv_treeA_proper:
Proper (equiv ==> equiv ==> equiv) treeA.
Proof.
cbv. now constructor.
Qed.
Discrimination law
Lemma equiv_empty s t:
s == t -> s = 0 <-> t = 0.
Proof.
induction 1; intuition congruence.
Qed.
Fact tdiscrim s t:
~ s@t == 0.
Proof.
intros A % equiv_empty. intuition congruence.
Qed.
Membership law
Inductive eltd s : tree -> Prop :=
| eltdH t: eltd s (s@t)
| eltdT t u : eltd s u -> eltd s (t@u).
Notation "s 'eld' t" := (eltd s t) (at level 70). (* s ⋵ t *)
Fact adj_eld s t u :
s eld t@u <-> s = t \/ s eld u.
Proof.
split.
- intros A. inv A; eauto.
- intros [-> |A]; now constructor.
Qed.
Definition incl s t := forall u, u eld s -> exists v, v eld t /\ u == v.
Fact incl_trans s t u :
incl s t -> incl t u -> incl s u.
Proof.
intros A B x C.
apply A in C as (y&C&D).
apply B in C as (z&C&E).
eauto using equiv.
Qed.
Ltac eld_inv :=
try match goal with
|[A: (_ eld _ @ _) |- _ ] =>
apply adj_eld in A as [->|A]
|[A: (_ eld ?s), B: incl ?s _ |- _ ] =>
apply B in A as (?&?&?)
end.
Lemma equiv_incl s t:
s == t -> incl s t /\ incl t s.
Proof.
intros A.
induction A as [s t | s t u| s s' t t' A IH1 B IH2 |
s |s t _ IH |s t u _ IH1 _ IH2 ];
try solve [ unfold incl; intuition; do 2 eld_inv;
eauto using eltd, equiv].
intuition eauto using incl_trans.
Qed.
Lemma eld_elt s t:
s eld t -> s elt t.
Proof.
induction 1; eauto using equiv.
Qed.
Fact tmember u s t:
u elt s@t -> u == s \/ u elt t.
Proof.
intros (A&_) % equiv_incl.
destruct (A u) as (v&B&C).
- auto using eltd.
- apply adj_eld in B as [<-|B].
+ auto.
+ right. rewrite C. apply eld_elt, B.
Qed.
Lexical tree ordering
Inductive lto : tree -> tree -> Prop :=
| ltoE s t : lto 0 (s@t)
| ltoF s t u v : lto s u -> lto (s@t) (u@v)
| ltoS s t v : lto t v -> lto (s@t) (s@v).
Notation "s '<' t" := (lto s t).
Fact lto_trans s t u :
s < t -> t < u -> s < u.
Proof.
intros A. revert u.
induction A; intros ? B; inv B; auto using lto.
Qed.
Lemma lto_irrefl' s t :
s < t -> s <> t.
Proof.
induction 1; intros B; inv B; auto.
Qed.
Fact lto_irrefl s :
~ s < s.
Proof.
intros A. eapply lto_irrefl'; eauto.
Qed.
Fact lto_tricho s t :
(s < t) + (s = t) + (t < s).
Proof.
revert t.
induction s as [|s1 IHs1 s2 IHs2]; intros t;
induction t as [|t1 IHt1 t2 IHt2]; auto using lto.
- destruct (IHs1 t1) as [[?| -> ]|?]; auto using lto.
+ destruct (IHs2 t2) as [[?| -> ]|?]; auto using lto.
Qed.
Insertion, order-respecting and duplicate-avoiding
Fixpoint alpha s t : tree :=
match t with
| 0 => s@0
| u@t => match lto_tricho s u with
| inl (inl _) => s @ u @ t
| inl (inr _) => u @ t
| inr _ => u @ alpha s t
end
end.
Fact alpha_equiv s t:
alpha s t == s@t.
Proof.
induction t as [|u _ t IH]; cbn.
- reflexivity.
- destruct (lto_tricho s u) as [[_| <- ]|_].
+ reflexivity.
+ symmetry. apply equivCancel.
+ rewrite IH. apply equivSwap.
Qed.
Lemma alpha_null s :
alpha s 0 = s@0.
Proof.
reflexivity.
Qed.
Ltac lto_cycle :=
try match goal with
|[A: ?s < ?s |- _ ] =>
contradiction (lto_irrefl A)
|[A: _ < ?s, B: ?s < _ |- _ ] =>
contradiction (lto_irrefl (lto_trans A B))
|[A: _ < ?s, B: ?s < ?t, C: ?t < _ |- _ ] =>
contradiction (lto_irrefl (lto_trans (lto_trans A B) C))
end.
Lemma alpha_eq s t :
alpha s (s@t) = s@t.
Proof.
cbn. destruct (lto_tricho s s) as [[|]|];
subst; auto; lto_cycle.
Qed.
Lemma alpha_le s t u :
s < t -> alpha s (t@u) = s@t@u.
Proof.
intros A. cbn.
destruct (lto_tricho s t) as [[|]|];
subst; auto; lto_cycle.
Qed.
Lemma alpha_ge u s t :
t < s -> alpha s (t@u) = t @ alpha s u.
Proof.
intros A. cbn.
destruct (lto_tricho s t) as [[|]|];
subst; auto; lto_cycle.
Qed.
Fact alpha_cancel s t:
alpha s (alpha s t) = alpha s t.
Proof.
induction t as [|u _ t IH].
- now rewrite !alpha_null, alpha_eq.
- destruct (lto_tricho s u) as [[A| <- ]|A];
repeat (rewrite (alpha_le _ A) || rewrite (alpha_ge _ A) || rewrite alpha_eq);
intuition congruence.
Qed.
Fact alpha_swap s t u:
alpha s (alpha t u) = alpha t (alpha s u).
Proof.
induction u as [|u _ v IH].
- destruct (lto_tricho s t) as [[A| <- ]|A];
repeat (rewrite (alpha_le _ A) || rewrite (alpha_ge _ A) || rewrite alpha_null);
auto.
- destruct (lto_tricho s u) as [[A| <- ]|A];
try destruct (lto_tricho t u) as [[B| <- ]|B];
destruct (lto_tricho s t) as [[C| <- ]|C];
repeat (rewrite (alpha_le _ A) || rewrite (alpha_ge _ A)
|| rewrite (alpha_le _ B) || rewrite (alpha_ge _ B)
|| rewrite (alpha_le _ C) || rewrite (alpha_ge _ C)
|| rewrite alpha_eq);
(lto_cycle || intuition congruence).
Qed.
Tree normalizer, based on lexical tree order-sorting
Fixpoint sigma s := match s with
| 0 => 0
| s@t => alpha (sigma s) (sigma t)
end.
Fact sigma_equiv s :
sigma s == s.
Proof.
induction s as [|s IHs t IHt]; cbn.
- reflexivity.
- now rewrite alpha_equiv, IHs, IHt.
Qed.
Fact sigma_equiv_eq s t:
s == t <-> sigma s = sigma t.
Proof.
split; intros A.
- induction A; cbn; try congruence.
+ apply alpha_cancel.
+ apply alpha_swap.
- now rewrite <- (sigma_equiv s), <- (sigma_equiv t), A.
Qed.
Fact sigma_idem s:
sigma (sigma s) = sigma s.
Proof.
apply sigma_equiv_eq, sigma_equiv.
Qed.
Fact equiv_dec s t:
dec (s == t).
Proof.
apply (dec_trans (sigma s = sigma t)).
- now rewrite sigma_equiv_eq.
- auto.
Qed.
Model construction
Theorem tree_model :
Sigma (X: HF) (S: tree -> X) (I: X -> tree),
(forall x, S (I x) = x) /\
(forall s, I (S s) == s) /\
(forall s t, S s = S t <-> s == t) /\
(forall x y, I x = I y <-> x = y) /\
(forall s t, S (s@t) = adj (S s) (S t)) /\
(forall x y, I (adj x y) == I x @ I y) /\
S 0 = eset /\
I eset = 0.
Proof.
destruct (@sub_norm (EqType tree) sigma sigma_idem) as (X&S&I&SI&IS).
pose (eset := S 0).
pose (adj x y := S (I x @ I y)).
assert (IS' : forall s, I (S s) == s).
{ intros s. rewrite IS. apply sigma_equiv. }
assert (I_agree : forall x y, I x = I y <-> x = y).
{ intuition congruence. }
assert (S_agree : forall s t, S s = S t <-> s == t).
{ intros s t. rewrite <- I_agree, !IS. symmetry. apply sigma_equiv_eq. }
assert (S_homo : forall s t, S (s@t) = adj (S s) (S t)).
{ intros s t. apply S_agree. now rewrite !IS'. }
assert (I_homo : forall x y, I (adj x y) == I x @ I y).
{ intros x y. apply S_agree. now rewrite SI. }
assert (S0 : S 0 = eset).
{ reflexivity. }
assert (I0 : I eset = 0).
{ destruct (I eset) as [|s t] eqn:A. reflexivity.
contradiction (@tdiscrim s t). apply S_agree. congruence. }
assert (cancel: forall x y, adj x (adj x y) = adj x y).
{ intros x y. apply S_agree. unfold adj. rewrite IS'. apply equivCancel. }
assert (swap: forall x y z, adj x (adj y z) = adj y (adj x z)).
{ intros x y z. apply S_agree. unfold adj. rewrite !IS'. apply equivSwap. }
assert (discrim: forall x y, adj x y <> eset).
{ unfold adj, eset. intros x y A % S_agree. contradiction (tdiscrim A). }
assert (member: forall x y z, adj x (adj y z) = adj y z -> x = y \/ adj x z = z).
{ intros x y z. unfold adj. rewrite IS, S_agree, sigma_equiv.
intros [A|A] % tmember.
+ left. now rewrite <- S_agree, !SI in A.
+ right. now rewrite <- S_agree, !SI in A. }
pose (XS := HFS (SI2sip SI S0 S_homo) swap cancel discrim member).
exists XS, S, I. tauto.
Qed.
Extensionality of tree equivalence