lexico.v 5.86 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
2 3 4
(* 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. *)
5
From stdpp Require Import numbers.
6
Set Default Proof Using "Type".
7 8 9 10 11 12 13 14

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

15 16 17
Instance prod_lexico `{Lexico A, Lexico B} : Lexico (A * B) := λ p1 p2,
  (**i 1.) *) lexico (p1.1) (p2.1) 
  (**i 2.) *) p1.1 = p2.1  lexico (p1.2) (p2.2).
18

19 20 21 22 23
Instance bool_lexico : Lexico bool := λ b1 b2,
  match b1, b2 with false, true => True | _, _ => False end.
Instance nat_lexico : Lexico nat := (<).
Instance N_lexico : Lexico N := (<)%N.
Instance Z_lexico : Lexico Z := (<)%Z.
24 25 26 27 28
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
29
  | [], _ :: _ => True
30
  | x1 :: l1, x2 :: l2 => lexico (x1,l1) (x2,l2)
31
  | _, _ => False
32 33 34 35
  end.
Instance sig_lexico `{Lexico A} (P : A  Prop) `{ x, ProofIrrel (P x)} :
  Lexico (sig P) := λ x1 x2, lexico (`x1) (`x2).

36 37
Lemma prod_lexico_irreflexive `{Lexico A, Lexico B, !Irreflexive (@lexico A _)}
  (x : A) (y : B) : complement lexico y y  complement lexico (x,y) (x,y).
38
Proof. intros ? [?|[??]]. by apply (irreflexivity lexico x). done. Qed.
39 40
Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)}
    (x1 x2 x3 : A) (y1 y2 y3 : B) :
41 42 43 44
  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.
45
  intros [|[??]] [?|[??]]; simplify_eq/=; auto.
46
  by left; trans x2.
47
Qed.
48

49
Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
50
  `{!StrictOrder (@lexico B _)} : StrictOrder (@lexico (A * B) _).
51
Proof.
52
  split.
53
  - intros [x y]. apply prod_lexico_irreflexive.
54
    by apply (irreflexivity lexico y).
55
  - intros [??] [??] [??] ??.
Ralf Jung's avatar
Ralf Jung committed
56
    eapply prod_lexico_transitive; eauto. apply transitivity.
57
Qed.
58 59
Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
  `{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
60 61
Proof.
 red; refine (λ p1 p2,
62
  match trichotomyT lexico (p1.1) (p2.1) with
63
  | inleft (left _) => inleft (left _)
64
  | inleft (right _) => cast_trichotomy (trichotomyT lexico (p1.2) (p2.2))
65
  | inright _ => inright _
66 67
  end); clear tA tB;
    abstract (unfold lexico, prod_lexico; auto using injective_projections).
68 69
Defined.

70 71
Instance bool_lexico_po : StrictOrder (@lexico bool _).
Proof. split. by intros [] ?. by intros [] [] [] ??. Qed.
72 73 74 75 76 77 78 79 80 81 82
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.

83
Instance nat_lexico_po : StrictOrder (@lexico nat _).
84 85 86 87 88
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
89
  | Lt => λ H, inleft (left (nat_compare_Lt_lt _ _ H))
90
  | Eq => λ H, inleft (right (nat_compare_eq _ _ H))
91
  | Gt => λ H, inright (nat_compare_Gt_gt _ _ H)
92 93 94
  end eq_refl).
Defined.

95
Instance N_lexico_po : StrictOrder (@lexico N _).
96 97 98 99 100
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
101
  | Lt => λ H, inleft (left (proj2 (N.compare_lt_iff _ _) H))
102
  | Eq => λ H, inleft (right (N.compare_eq _ _ H))
103
  | Gt => λ H, inright (proj1 (N.compare_gt_iff _ _) H)
104 105 106
  end eq_refl).
Defined.

107
Instance Z_lexico_po : StrictOrder (@lexico Z _).
108 109 110 111 112
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
113
  | Lt => λ H, inleft (left (proj2 (Z.compare_lt_iff _ _) H))
114
  | Eq => λ H, inleft (right (Z.compare_eq _ _ H))
115
  | Gt => λ H, inright (proj1 (Z.compare_gt_iff _ _) H)
116 117 118
  end eq_refl).
Defined.

119
Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
120
  StrictOrder (@lexico (list A) _).
121
Proof.
122
  split.
123 124
  - intros l. induction l. by intros ?. by apply prod_lexico_irreflexive.
  - intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
125 126
    eapply prod_lexico_transitive; eauto.
Qed.
127
Instance list_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} :
128 129 130 131 132 133 134 135 136 137
  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))
138 139
  end); clear tA go go';
    abstract (repeat (done || constructor || congruence || by inversion 1)).
140 141
Defined.

142
Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
143
  (P : A  Prop) `{ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
144
Proof.
145
  unfold lexico, sig_lexico. split.
146
  - intros [x ?] ?. by apply (irreflexivity lexico x). 
147
  - intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
148
Qed.
149
Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
150 151 152 153 154
  (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.