lexico.v 7.31 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
Require Import orders.

Notation cast_trichotomy T :=
  match T with
  | inleft (left _) => inleft (left _)
  | inleft (right _) => inleft (right _)
  | inright _ => inright _
  end.

Instance prod_lexico `{Lexico A} `{Lexico B} : Lexico (A * B) := λ p1 p2,
  (**i 1.) *) strict lexico (fst p1) (fst p2) 
  (**i 2.) *) fst p1 = fst p2  lexico (snd p1) (snd p2).

Lemma prod_lexico_strict `{Lexico A} `{Lexico B} (p1 p2 : A * B) :
  strict lexico p1 p2 
    strict lexico (fst p1) (fst p2) 
    fst p1 = fst p2  strict lexico (snd p1) (snd p2).
Proof.
  destruct p1, p2. repeat (unfold lexico, prod_lexico, strict). naive_solver.
Qed.

Instance bool_lexico : Lexico bool := ().
Instance nat_lexico : Lexico nat := ().
Instance N_lexico : Lexico N := ()%N.
Instance Z_lexico : Lexico Z := ()%Z.
Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
Instance list_lexico `{Lexico A} : Lexico (list A) :=
  fix go l1 l2 :=
  let _ : Lexico (list A) := @go in
  match l1, l2 with
  | [], _ => True
  | _ :: _, [] => False
  | x1 :: l1, x2 :: l2 => lexico (x1,l1) (x2,l2)
  end.
Instance sig_lexico `{Lexico A} (P : A  Prop) `{ x, ProofIrrel (P x)} :
  Lexico (sig P) := λ x1 x2, lexico (`x1) (`x2).

Lemma prod_lexico_reflexive `{Lexico A} `{!PartialOrder (@lexico A _)}
  `{Lexico B} (x : A) (y : B) : lexico y y  lexico (x,y) (x,y).
Proof. by right. Qed.
Lemma prod_lexico_transitive `{Lexico A} `{!PartialOrder (@lexico A _)}
    `{Lexico B} (x1 x2 x3 : A) (y1 y2 y3 : B) :
  lexico (x1,y1) (x2,y2)  lexico (x2,y2) (x3,y3) 
  (lexico y1 y2  lexico y2 y3  lexico y1 y3)  lexico (x1,y1) (x3,y3).
Proof.
  intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico.
  intros [|[??]] [?|[??]]; simplify_equality'; auto. left. by transitivity x2.
Qed.
Lemma prod_lexico_anti_symmetric `{Lexico A} `{!PartialOrder (@lexico A _)}
    `{Lexico B} (x1 x2 : A) (y1 y2 : B) :
  lexico (x1,y1) (x2,y2)  lexico (x2,y2) (x1,y1) 
  (lexico y1 y2  lexico y2 y1  y1 = y2)  x1 = x2  y1 = y2.
Proof. by intros [[??]|[??]] [[??]|[??]] ?; simplify_equality'; auto. Qed.
Instance prod_lexico_po `{Lexico A} `{Lexico B} `{!PartialOrder (@lexico A _)}
  `{!PartialOrder (@lexico B _)} : PartialOrder (@lexico (A * B) _).
Proof.
  repeat split.
  * by intros [??]; apply prod_lexico_reflexive.
  * intros [??] [??] [??] ??.
    eapply prod_lexico_transitive; eauto. apply @transitivity, _.
  * intros [x1 y1] [x2 y2] ??.
    destruct (prod_lexico_anti_symmetric x1 x2 y1 y2); try intuition congruence.
    apply (anti_symmetric _).
Qed.
Instance prod_lexico_trichotomyT `{Lexico A} `{tA: !TrichotomyT (@lexico A _)}
  `{Lexico B} `{tB:!TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
Proof.
 red; refine (λ p1 p2,
  match trichotomyT lexico (fst p1) (fst p2) with
  | inleft (left _) => inleft (left _)
  | inleft (right _) =>
    cast_trichotomy (trichotomyT lexico (snd p1) (snd p2))
  | inright _ => inright _
  end); clear tA tB; abstract (rewrite ?prod_lexico_strict;
    intuition (auto using injective_projections with congruence)).
Defined.

Instance bool_lexico_po : PartialOrder (@lexico bool _).
Proof.
  unfold lexico, bool_lexico. repeat split.
  * intros []; simpl; tauto.
  * intros [] [] []; simpl; tauto.
  * intros [] []; simpl; tauto.
Qed.
Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
Proof.
 red; refine (λ b1 b2,
  match b1, b2 with
  | false, false => inleft (right _)
  | false, true => inleft (left _)
  | true, false => inright _
  | true, true => inleft (right _)
  end); abstract (unfold strict, lexico, bool_lexico; naive_solver).
Defined.

Lemma nat_lexico_strict (x1 x2 : nat) : strict lexico x1 x2  x1 < x2.
Proof. unfold strict, lexico, nat_lexico. lia. Qed.
Instance nat_lexico_po : PartialOrder (@lexico nat _).
Proof. unfold lexico, nat_lexico. apply _. Qed.
Instance nat_lexico_trichotomy: TrichotomyT (@lexico nat _).
Proof.
 red; refine (λ n1 n2,
  match Nat.compare n1 n2 as c return Nat.compare n1 n2 = c  _ with
  | Lt => λ H,
    inleft (left (proj2 (nat_lexico_strict _ _) (nat_compare_Lt_lt _ _ H)))
  | Eq => λ H, inleft (right (nat_compare_eq _ _ H))
  | Gt => λ H,
    inright (proj2 (nat_lexico_strict _ _) (nat_compare_Gt_gt _ _ H))
  end eq_refl).
Defined.

Lemma N_lexico_strict (x1 x2 : N) : strict lexico x1 x2  (x1 < x2)%N.
Proof. unfold strict, lexico, N_lexico. lia. Qed.
Instance N_lexico_po : PartialOrder (@lexico N _).
Proof. unfold lexico, N_lexico. apply _. Qed.
Instance N_lexico_trichotomy: TrichotomyT (@lexico N _).
Proof.
 red; refine (λ n1 n2,
  match N.compare n1 n2 as c return N.compare n1 n2 = c  _ with
  | Lt => λ H,
    inleft (left (proj2 (N_lexico_strict _ _) (proj2 (N.compare_lt_iff _ _) H)))
  | Eq => λ H, inleft (right (N.compare_eq _ _ H))
  | Gt => λ H,
    inright (proj2 (N_lexico_strict _ _) (proj1 (N.compare_gt_iff _ _) H))
  end eq_refl).
Defined.

Lemma Z_lexico_strict (x1 x2 : Z) : strict lexico x1 x2  (x1 < x2)%Z.
Proof. unfold strict, lexico, Z_lexico. lia. Qed.
Instance Z_lexico_po : PartialOrder (@lexico Z _).
Proof. unfold lexico, Z_lexico. apply _. Qed.
Instance Z_lexico_trichotomy: TrichotomyT (@lexico Z _).
Proof.
 red; refine (λ n1 n2,
  match Z.compare n1 n2 as c return Z.compare n1 n2 = c  _ with
  | Lt => λ H,
    inleft (left (proj2 (Z_lexico_strict _ _) (proj2 (Z.compare_lt_iff _ _) H)))
  | Eq => λ H, inleft (right (Z.compare_eq _ _ H))
  | Gt => λ H,
    inright (proj2 (Z_lexico_strict _ _) (proj1 (Z.compare_gt_iff _ _) H))
  end eq_refl).
Defined.

Instance list_lexico_po `{Lexico A} `{!PartialOrder (@lexico A _)} :
  PartialOrder (@lexico (list A) _).
Proof.
  repeat split.
  * intros l. induction l. done. by apply prod_lexico_reflexive.
  * intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
    eapply prod_lexico_transitive; eauto.
  * intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] ??; try done.
    destruct (prod_lexico_anti_symmetric x1 x2 l1 l2); naive_solver.
Qed.
Instance list_lexico_trichotomy `{Lexico A} `{!TrichotomyT (@lexico A _)} :
  TrichotomyT (@lexico (list A) _).
Proof.
 refine (
  fix go l1 l2 :=
  let go' : TrichotomyT (@lexico (list A) _) := @go in
  match l1, l2 with
  | [], [] => inleft (right _)
  | [], _ :: _ => inleft (left _)
  | _ :: _, [] => inright _
  | x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
  end); clear go go';
  abstract (repeat (done || constructor || congruence || by inversion 1)).
Defined.

Instance sig_lexico_po `{Lexico A} `{!PartialOrder (@lexico A _)}
  (P : A  Prop) `{ x, ProofIrrel (P x)} : PartialOrder (@lexico (sig P) _).
Proof.
  unfold lexico, sig_lexico. repeat split.
  * by intros [??].
  * intros [x1 ?] [x2 ?] [x3 ?] ??. by simplify_order.
  * intros [x1 ?] [x2 ?] ??. apply (sig_eq_pi _). by simplify_order.
Qed.
Instance sig_lexico_trichotomy `{Lexico A} `{tA: !TrichotomyT (@lexico A _)}
  (P : A  Prop) `{ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
Proof.
 red; refine (λ x1 x2, cast_trichotomy (trichotomyT lexico (`x1) (`x2)));
  abstract (repeat (done || constructor || apply (sig_eq_pi P))).
Defined.