Commit f7f79d26 authored by Ralf Jung's avatar Ralf Jung

add tactic aliases: trans -> transitivity; etrans -> etransitivity

parent 42e3e6de
...@@ -60,7 +60,7 @@ Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m). ...@@ -60,7 +60,7 @@ Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
Proof. rewrite (dom_insert _). set_solver. Qed. Proof. rewrite (dom_insert _). set_solver. Qed.
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X : Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
X dom D m X dom D (<[i:=x]>m). X dom D m X dom D (<[i:=x]>m).
Proof. intros. transitivity (dom D m); eauto using dom_insert_subseteq. Qed. Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]} {[ i ]}. Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]} {[ i ]}.
Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed. Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
Lemma dom_delete {A} (m : M A) i : dom D (delete i m) dom D m {[ i ]}. Lemma dom_delete {A} (m : M A) i : dom D (delete i m) dom D m {[ i ]}.
......
...@@ -123,7 +123,7 @@ Section setoid. ...@@ -123,7 +123,7 @@ Section setoid.
split. split.
- by intros m i. - by intros m i.
- by intros m1 m2 ? i. - by intros m1 m2 ? i.
- by intros m1 m2 m3 ?? i; transitivity (m2 !! i). - by intros m1 m2 m3 ?? i; trans (m2 !! i).
Qed. Qed.
Global Instance lookup_proper (i : K) : Global Instance lookup_proper (i : K) :
Proper (() ==> ()) (lookup (M:=M A) i). Proper (() ==> ()) (lookup (M:=M A) i).
...@@ -199,7 +199,7 @@ Proof. ...@@ -199,7 +199,7 @@ Proof.
split; [intros m i; by destruct (m !! i); simpl|]. split; [intros m i; by destruct (m !! i); simpl|].
intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i). intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=; destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
done || etransitivity; eauto. done || etrans; eauto.
Qed. Qed.
Global Instance: PartialOrder (() : relation (M A)). Global Instance: PartialOrder (() : relation (M A)).
Proof. Proof.
...@@ -1182,10 +1182,10 @@ Proof. ...@@ -1182,10 +1182,10 @@ Proof.
intros. rewrite map_union_comm by done. by apply map_union_subseteq_l. intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
Qed. Qed.
Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 m2 m1 m2 m3. Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 m2 m1 m2 m3.
Proof. intros. transitivity m2; auto using map_union_subseteq_l. Qed. Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) : Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
m2 m3 m1 m3 m1 m2 m3. m2 m3 m1 m3 m1 m2 m3.
Proof. intros. transitivity m3; auto using map_union_subseteq_r. Qed. Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
Lemma map_union_preserving_l {A} (m1 m2 m3 : M A) : m1 m2 m3 m1 m3 m2. Lemma map_union_preserving_l {A} (m1 m2 m3 : M A) : m1 m2 m3 m1 m3 m2.
Proof. Proof.
rewrite !map_subseteq_spec. intros ???. rewrite !map_subseteq_spec. intros ???.
......
...@@ -42,7 +42,7 @@ Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)} ...@@ -42,7 +42,7 @@ Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)}
Proof. Proof.
intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico. intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico.
intros [|[??]] [?|[??]]; simplify_eq/=; auto. intros [|[??]] [?|[??]]; simplify_eq/=; auto.
by left; transitivity x2. by left; trans x2.
Qed. Qed.
Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)} Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
...@@ -52,7 +52,7 @@ Proof. ...@@ -52,7 +52,7 @@ Proof.
- intros [x y]. apply prod_lexico_irreflexive. - intros [x y]. apply prod_lexico_irreflexive.
by apply (irreflexivity lexico y). by apply (irreflexivity lexico y).
- intros [??] [??] [??] ??. - intros [??] [??] [??] ??.
eapply prod_lexico_transitive; eauto. apply transitivity. eapply prod_lexico_transitive; eauto. apply trans.
Qed. Qed.
Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)} Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
`{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _). `{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
...@@ -143,7 +143,7 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} ...@@ -143,7 +143,7 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
Proof. Proof.
unfold lexico, sig_lexico. split. unfold lexico, sig_lexico. split.
- intros [x ?] ?. by apply (irreflexivity lexico x). - intros [x ?] ?. by apply (irreflexivity lexico x).
- intros [x1 ?] [x2 ?] [x3 ?] ??. by transitivity x2. - intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
Qed. Qed.
Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
(P : A Prop) `{ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _). (P : A Prop) `{ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
......
...@@ -371,7 +371,7 @@ Section setoid. ...@@ -371,7 +371,7 @@ Section setoid.
- intros l; induction l; constructor; auto. - intros l; induction l; constructor; auto.
- induction 1; constructor; auto. - induction 1; constructor; auto.
- intros l1 l2 l3 Hl; revert l3. - intros l1 l2 l3 Hl; revert l3.
induction Hl; inversion_clear 1; constructor; try etransitivity; eauto. induction Hl; inversion_clear 1; constructor; try etrans; eauto.
Qed. Qed.
Global Instance cons_proper : Proper (() ==> () ==> ()) (@cons A). Global Instance cons_proper : Proper (() ==> () ==> ()) (@cons A).
Proof. by constructor. Qed. Proof. by constructor. Qed.
...@@ -1719,7 +1719,7 @@ Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed. ...@@ -1719,7 +1719,7 @@ Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed.
Lemma sublist_foldr_delete l is : foldr delete l is `sublist` l. Lemma sublist_foldr_delete l is : foldr delete l is `sublist` l.
Proof. Proof.
induction is as [|i is IH]; simpl; [done |]. induction is as [|i is IH]; simpl; [done |].
transitivity (foldr delete l is); auto using sublist_delete. trans (foldr delete l is); auto using sublist_delete.
Qed. Qed.
Lemma sublist_alt l1 l2 : l1 `sublist` l2 is, l1 = foldr delete l2 is. Lemma sublist_alt l1 l2 : l1 `sublist` l2 is, l1 = foldr delete l2 is.
Proof. Proof.
...@@ -1749,7 +1749,7 @@ Proof. ...@@ -1749,7 +1749,7 @@ Proof.
+ by rewrite !Permutation_middle, Permutation_swap. + by rewrite !Permutation_middle, Permutation_swap.
- intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial. - intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''. destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''.
split. done. etransitivity; eauto. split. done. etrans; eauto.
Qed. Qed.
Lemma sublist_Permutation l1 l2 l3 : Lemma sublist_Permutation l1 l2 l3 :
l1 `sublist` l2 l2 l3 l4, l1 l4 l4 `sublist` l3. l1 `sublist` l2 l2 l3 l4, l1 l4 l4 `sublist` l3.
...@@ -1770,7 +1770,7 @@ Proof. ...@@ -1770,7 +1770,7 @@ Proof.
+ exists (x :: y :: l1''). by repeat constructor. + exists (x :: y :: l1''). by repeat constructor.
- intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial. - intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial.
destruct (IH2 l3') as (l3'' &?&?); trivial. exists l3''. destruct (IH2 l3') as (l3'' &?&?); trivial. exists l3''.
split; [|done]. etransitivity; eauto. split; [|done]. etrans; eauto.
Qed. Qed.
(** Properties of the [contains] predicate *) (** Properties of the [contains] predicate *)
...@@ -1816,10 +1816,10 @@ Proof. intro. apply contains_Permutation_length_le. lia. Qed. ...@@ -1816,10 +1816,10 @@ Proof. intro. apply contains_Permutation_length_le. lia. Qed.
Global Instance: Proper (() ==> () ==> iff) (@contains A). Global Instance: Proper (() ==> () ==> iff) (@contains A).
Proof. Proof.
intros l1 l2 ? k1 k2 ?. split; intros. intros l1 l2 ? k1 k2 ?. split; intros.
- transitivity l1. by apply Permutation_contains. - trans l1. by apply Permutation_contains.
transitivity k1. done. by apply Permutation_contains. trans k1. done. by apply Permutation_contains.
- transitivity l2. by apply Permutation_contains. - trans l2. by apply Permutation_contains.
transitivity k2. done. by apply Permutation_contains. trans k2. done. by apply Permutation_contains.
Qed. Qed.
Global Instance: AntiSymm () (@contains A). Global Instance: AntiSymm () (@contains A).
Proof. red. auto using contains_Permutation_length_le, contains_length. Qed. Proof. red. auto using contains_Permutation_length_le, contains_length. Qed.
...@@ -1842,9 +1842,9 @@ Proof. ...@@ -1842,9 +1842,9 @@ Proof.
- intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor. - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
- intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?). - intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?).
destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial. destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial.
exists l3'. split; etransitivity; eauto. } exists l3'. split; etrans; eauto. }
intros (l2&?&?). intros (l2&?&?).
transitivity l2; auto using sublist_contains, Permutation_contains. trans l2; auto using sublist_contains, Permutation_contains.
Qed. Qed.
Lemma contains_sublist_r l1 l3 : Lemma contains_sublist_r l1 l3 :
l1 `contains` l3 l2, l1 l2 l2 `sublist` l3. l1 `contains` l3 l2, l1 l2 l2 `sublist` l3.
...@@ -1863,7 +1863,7 @@ Proof. rewrite !(comm (++) _ k). apply contains_skips_l. Qed. ...@@ -1863,7 +1863,7 @@ Proof. rewrite !(comm (++) _ k). apply contains_skips_l. Qed.
Lemma contains_app l1 l2 k1 k2 : Lemma contains_app l1 l2 k1 k2 :
l1 `contains` l2 k1 `contains` k2 l1 ++ k1 `contains` l2 ++ k2. l1 `contains` l2 k1 `contains` k2 l1 ++ k1 `contains` l2 ++ k2.
Proof. Proof.
transitivity (l1 ++ k2); auto using contains_skips_l, contains_skips_r. trans (l1 ++ k2); auto using contains_skips_l, contains_skips_r.
Qed. Qed.
Lemma contains_cons_r x l k : Lemma contains_cons_r x l k :
l `contains` x :: k l `contains` k l', l x :: l' l' `contains` k. l `contains` x :: k l `contains` k l', l x :: l' l' `contains` k.
...@@ -1975,7 +1975,7 @@ Section contains_dec. ...@@ -1975,7 +1975,7 @@ Section contains_dec.
- simplify_option_eq; eauto using Permutation_swap. - simplify_option_eq; eauto using Permutation_swap.
- destruct (IH1 k1) as (k2&?&?); trivial. - destruct (IH1 k1) as (k2&?&?); trivial.
destruct (IH2 k2) as (k3&?&?); trivial. destruct (IH2 k2) as (k3&?&?); trivial.
exists k3. split; eauto. by transitivity k2. exists k3. split; eauto. by trans k2.
Qed. Qed.
Lemma list_remove_Some l k x : list_remove x l = Some k l x :: k. Lemma list_remove_Some l k x : list_remove x l = Some k l x :: k.
Proof. Proof.
...@@ -2493,7 +2493,7 @@ Section Forall2_order. ...@@ -2493,7 +2493,7 @@ Section Forall2_order.
Global Instance: Symmetric R Symmetric (Forall2 R). Global Instance: Symmetric R Symmetric (Forall2 R).
Proof. intros. induction 1; constructor; auto. Qed. Proof. intros. induction 1; constructor; auto. Qed.
Global Instance: Transitive R Transitive (Forall2 R). Global Instance: Transitive R Transitive (Forall2 R).
Proof. intros ????. apply Forall2_transitive. by apply @transitivity. Qed. Proof. intros ????. apply Forall2_transitive. by apply @trans. Qed.
Global Instance: Equivalence R Equivalence (Forall2 R). Global Instance: Equivalence R Equivalence (Forall2 R).
Proof. split; apply _. Qed. Proof. split; apply _. Qed.
Global Instance: PreOrder R PreOrder (Forall2 R). Global Instance: PreOrder R PreOrder (Forall2 R).
...@@ -2768,14 +2768,14 @@ Section bind. ...@@ -2768,14 +2768,14 @@ Section bind.
- by apply contains_app. - by apply contains_app.
- by rewrite !(assoc_L (++)), (comm (++) (f _)). - by rewrite !(assoc_L (++)), (comm (++) (f _)).
- by apply contains_inserts_l. - by apply contains_inserts_l.
- etransitivity; eauto. - etrans; eauto.
Qed. Qed.
Global Instance bind_Permutation: Proper (() ==> ()) (mbind f). Global Instance bind_Permutation: Proper (() ==> ()) (mbind f).
Proof. Proof.
induction 1; csimpl; auto. induction 1; csimpl; auto.
- by f_equiv. - by f_equiv.
- by rewrite !(assoc_L (++)), (comm (++) (f _)). - by rewrite !(assoc_L (++)), (comm (++) (f _)).
- etransitivity; eauto. - etrans; eauto.
Qed. Qed.
Lemma bind_cons x l : (x :: l) = f = f x ++ l = f. Lemma bind_cons x l : (x :: l) = f = f x ++ l = f.
Proof. done. Qed. Proof. done. Qed.
...@@ -2998,7 +2998,7 @@ Lemma foldr_permutation {A B} (R : relation B) `{!Equivalence R} ...@@ -2998,7 +2998,7 @@ Lemma foldr_permutation {A B} (R : relation B) `{!Equivalence R}
(f : A B B) (b : B) `{!Proper ((=) ==> R ==> R) f} (f : A B B) (b : B) `{!Proper ((=) ==> R ==> R) f}
(Hf : a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) : (Hf : a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper (() ==> R) (foldr f b). Proper (() ==> R) (foldr f b).
Proof. induction 1; simpl; [done|by f_equiv|apply Hf|etransitivity; eauto]. Qed. Proof. induction 1; simpl; [done|by f_equiv|apply Hf|etrans; eauto]. Qed.
(** ** Properties of the [zip_with] and [zip] functions *) (** ** Properties of the [zip_with] and [zip] functions *)
Section zip_with. Section zip_with.
......
...@@ -243,7 +243,7 @@ Proof. ...@@ -243,7 +243,7 @@ Proof.
intros [??] ?. intros [??] ?.
destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |]. destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |]. destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
split. apply Z.quot_pos; lia. transitivity x; auto. apply Z.quot_lt; lia. split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia.
Qed. Qed.
(* Note that we cannot disable simpl for [Z.of_nat] as that would break (* Note that we cannot disable simpl for [Z.of_nat] as that would break
...@@ -396,7 +396,7 @@ Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y. ...@@ -396,7 +396,7 @@ Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y.
Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed. Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 x 0 y 0 x + y. Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 x 0 y 0 x + y.
Proof. Proof.
intros. transitivity (x + 0); [by rewrite Qcplus_0_r|]. intros. trans (x + 0); [by rewrite Qcplus_0_r|].
by apply Qcplus_le_mono_l. by apply Qcplus_le_mono_l.
Qed. Qed.
Lemma Qcplus_neg_nonpos (x y : Qc) : x < 0 y 0 x + y < 0. Lemma Qcplus_neg_nonpos (x y : Qc) : x < 0 y 0 x + y < 0.
...@@ -410,7 +410,7 @@ Lemma Qcplus_neg_neg (x y : Qc) : x < 0 → y < 0 → x + y < 0. ...@@ -410,7 +410,7 @@ Lemma Qcplus_neg_neg (x y : Qc) : x < 0 → y < 0 → x + y < 0.
Proof. auto using Qcplus_nonpos_neg, Qclt_le_weak. Qed. Proof. auto using Qcplus_nonpos_neg, Qclt_le_weak. Qed.
Lemma Qcplus_nonpos_nonpos (x y : Qc) : x 0 y 0 x + y 0. Lemma Qcplus_nonpos_nonpos (x y : Qc) : x 0 y 0 x + y 0.
Proof. Proof.
intros. transitivity (x + 0); [|by rewrite Qcplus_0_r]. intros. trans (x + 0); [|by rewrite Qcplus_0_r].
by apply Qcplus_le_mono_l. by apply Qcplus_le_mono_l.
Qed. Qed.
Lemma Qcmult_le_mono_nonneg_l x y z : 0 z x y z * x z * y. Lemma Qcmult_le_mono_nonneg_l x y z : 0 z x y z * x z * y.
...@@ -436,7 +436,7 @@ Proof. ...@@ -436,7 +436,7 @@ Proof.
Qed. Qed.
Lemma Qcmult_nonneg_nonneg x y : 0 x 0 y 0 x * y. Lemma Qcmult_nonneg_nonneg x y : 0 x 0 y 0 x * y.
Proof. Proof.
intros. transitivity (0 * y); [by rewrite Qcmult_0_l|]. intros. trans (0 * y); [by rewrite Qcmult_0_l|].
by apply Qcmult_le_mono_nonneg_r. by apply Qcmult_le_mono_nonneg_r.
Qed. Qed.
......
...@@ -96,7 +96,7 @@ Section setoids. ...@@ -96,7 +96,7 @@ Section setoids.
split. split.
- by intros []; constructor. - by intros []; constructor.
- by destruct 1; constructor. - by destruct 1; constructor.
- destruct 1; inversion 1; constructor; etransitivity; eauto. - destruct 1; inversion 1; constructor; etrans; eauto.
Qed. Qed.
Global Instance Some_proper : Proper (() ==> ()) (@Some A). Global Instance Some_proper : Proper (() ==> ()) (@Some A).
Proof. by constructor. Qed. Proof. by constructor. Qed.
......
...@@ -29,13 +29,13 @@ Section orders. ...@@ -29,13 +29,13 @@ Section orders.
Proof. by intros [??] <-. Qed. Proof. by intros [??] <-. Qed.
Lemma strict_transitive_l `{!Transitive R} X Y Z : X Y Y Z X Z. Lemma strict_transitive_l `{!Transitive R} X Y Z : X Y Y Z X Z.
Proof. Proof.
intros [? HXY] ?. split; [by transitivity Y|]. intros [? HXY] ?. split; [by trans Y|].
contradict HXY. by transitivity Z. contradict HXY. by trans Z.
Qed. Qed.
Lemma strict_transitive_r `{!Transitive R} X Y Z : X Y Y Z X Z. Lemma strict_transitive_r `{!Transitive R} X Y Z : X Y Y Z X Z.
Proof. Proof.
intros ? [? HYZ]. split; [by transitivity Y|]. intros ? [? HYZ]. split; [by trans Y|].
contradict HYZ. by transitivity X. contradict HYZ. by trans X.
Qed. Qed.
Global Instance: Irreflexive (strict R). Global Instance: Irreflexive (strict R).
Proof. firstorder. Qed. Proof. firstorder. Qed.
...@@ -79,7 +79,7 @@ Section strict_orders. ...@@ -79,7 +79,7 @@ Section strict_orders.
Proof. intros ->. apply (irreflexivity R). Qed. Proof. intros ->. apply (irreflexivity R). Qed.
Lemma strict_anti_symm `{!StrictOrder R} X Y : Lemma strict_anti_symm `{!StrictOrder R} X Y :
X Y Y X False. X Y Y X False.
Proof. intros. apply (irreflexivity R X). by transitivity Y. Qed. Proof. intros. apply (irreflexivity R X). by trans Y. Qed.
Global Instance trichotomyT_dec `{!TrichotomyT R, !StrictOrder R} X Y : Global Instance trichotomyT_dec `{!TrichotomyT R, !StrictOrder R} X Y :
Decision (X Y) := Decision (X Y) :=
match trichotomyT R X Y with match trichotomyT R X Y with
...@@ -101,7 +101,7 @@ Ltac simplify_order := repeat ...@@ -101,7 +101,7 @@ Ltac simplify_order := repeat
assert (x = y) by (by apply (anti_symm R)); clear H1 H2 assert (x = y) by (by apply (anti_symm R)); clear H1 H2
| H2 : R y ?z |- _ => | H2 : R y ?z |- _ =>
unless (R x z) by done; unless (R x z) by done;
assert (R x z) by (by transitivity y) assert (R x z) by (by trans y)
end end
end. end.
...@@ -319,13 +319,13 @@ Section preorder. ...@@ -319,13 +319,13 @@ Section preorder.
split. split.
- done. - done.
- by intros ?? [??]. - by intros ?? [??].
- by intros X Y Z [??] [??]; split; transitivity Y. - by intros X Y Z [??] [??]; split; trans Y.
Qed. Qed.
Global Instance: Proper (() ==> () ==> iff) (() : relation A). Global Instance: Proper (() ==> () ==> iff) (() : relation A).
Proof. Proof.
unfold equiv, preorder_equiv. intros X1 Y1 ? X2 Y2 ?. split; intro. unfold equiv, preorder_equiv. intros X1 Y1 ? X2 Y2 ?. split; intro.
- transitivity X1. tauto. transitivity X2; tauto. - trans X1. tauto. trans X2; tauto.
- transitivity Y1. tauto. transitivity Y2; tauto. - trans Y1. tauto. trans Y2; tauto.
Qed. Qed.
Lemma subset_spec (X Y : A) : X Y X Y X Y. Lemma subset_spec (X Y : A) : X Y X Y X Y.
Proof. Proof.
...@@ -376,9 +376,9 @@ Section join_semi_lattice. ...@@ -376,9 +376,9 @@ Section join_semi_lattice.
Hint Resolve subseteq_empty union_subseteq_l union_subseteq_r union_least. Hint Resolve subseteq_empty union_subseteq_l union_subseteq_r union_least.
Lemma union_subseteq_l_transitive X1 X2 Y : X1 X2 X1 X2 Y. Lemma union_subseteq_l_transitive X1 X2 Y : X1 X2 X1 X2 Y.
Proof. intros. transitivity X2; auto. Qed. Proof. intros. trans X2; auto. Qed.
Lemma union_subseteq_r_transitive X1 X2 Y : X1 X2 X1 Y X2. Lemma union_subseteq_r_transitive X1 X2 Y : X1 X2 X1 Y X2.
Proof. intros. transitivity X2; auto. Qed. Proof. intros. trans X2; auto. Qed.
Hint Resolve union_subseteq_l_transitive union_subseteq_r_transitive. Hint Resolve union_subseteq_l_transitive union_subseteq_r_transitive.
Lemma union_preserving_l X Y1 Y2 : Y1 Y2 X Y1 X Y2. Lemma union_preserving_l X Y1 Y2 : Y1 Y2 X Y1 X Y2.
Proof. auto. Qed. Proof. auto. Qed.
...@@ -436,7 +436,7 @@ Section join_semi_lattice. ...@@ -436,7 +436,7 @@ Section join_semi_lattice.
Proof. Proof.
split. split.
- intros HXY. split; apply equiv_empty; - intros HXY. split; apply equiv_empty;
by transitivity (X Y); [auto | rewrite HXY]. by trans (X Y); [auto | rewrite HXY].
- intros [HX HY]. by rewrite HX, HY, (left_id _ _). - intros [HX HY]. by rewrite HX, HY, (left_id _ _).
Qed. Qed.
Lemma empty_union_list Xs : Xs Forall ( ) Xs. Lemma empty_union_list Xs : Xs Forall ( ) Xs.
...@@ -502,9 +502,9 @@ Section meet_semi_lattice. ...@@ -502,9 +502,9 @@ Section meet_semi_lattice.
Hint Resolve intersection_subseteq_l intersection_subseteq_r Hint Resolve intersection_subseteq_l intersection_subseteq_r
intersection_greatest. intersection_greatest.
Lemma intersection_subseteq_l_transitive X1 X2 Y : X1 X2 X1 Y X2. Lemma intersection_subseteq_l_transitive X1 X2 Y : X1 X2 X1 Y X2.
Proof. intros. transitivity X1; auto. Qed. Proof. intros. trans X1; auto. Qed.
Lemma intersection_subseteq_r_transitive X1 X2 Y : X1 X2 Y X1 X2. Lemma intersection_subseteq_r_transitive X1 X2 Y : X1 X2 Y X1 X2.
Proof. intros. transitivity X1; auto. Qed. Proof. intros. trans X1; auto. Qed.
Hint Resolve intersection_subseteq_l_transitive Hint Resolve intersection_subseteq_l_transitive
intersection_subseteq_r_transitive. intersection_subseteq_r_transitive.
Lemma intersection_preserving_l X Y1 Y2 : Y1 Y2 X Y1 X Y2. Lemma intersection_preserving_l X Y1 Y2 : Y1 Y2 X Y1 X Y2.
......
...@@ -49,7 +49,7 @@ Proof. ...@@ -49,7 +49,7 @@ Proof.
intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros s. intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros s.
assert (x = 0 0 < x)%N as [->|?] by lia; [by rewrite pretty_N_go_0|]. assert (x = 0 0 < x)%N as [->|?] by lia; [by rewrite pretty_N_go_0|].
rewrite pretty_N_go_step by done. rewrite pretty_N_go_step by done.
etransitivity; [|by eapply IH, N.div_lt]; simpl; lia. } etrans; [|by eapply IH, N.div_lt]; simpl; lia. }
intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros y s s'. intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros y s s'.
assert ((x = 0 0 < x) (y = 0 0 < y))%N as [[->|?] [->|?]] by lia; assert ((x = 0 0 < x) (y = 0 0 < y))%N as [[->|?] [->|?]] by lia;
rewrite ?pretty_N_go_0, ?pretty_N_go_step, ?(pretty_N_go_step y) by done. rewrite ?pretty_N_go_0, ?pretty_N_go_step, ?(pretty_N_go_step y) by done.
......
...@@ -70,7 +70,7 @@ Section rtc. ...@@ -70,7 +70,7 @@ Section rtc.
Lemma rtc_once x y : R x y rtc R x y. Lemma rtc_once x y : R x y rtc R x y.
Proof. eauto. Qed. Proof. eauto. Qed.
Lemma rtc_r x y z : rtc R x y R y z rtc R x z. Lemma rtc_r x y z : rtc R x y R y z rtc R x z.
Proof. intros. etransitivity; eauto. Qed. Proof. intros. etrans; eauto. Qed.
Lemma rtc_inv x z : rtc R x z x = z y, R x y rtc R y z. Lemma rtc_inv x z : rtc R x z x = z y, R x y rtc R y z.
Proof. inversion_clear 1; eauto. Qed. Proof. inversion_clear 1; eauto. Qed.
Lemma rtc_ind_l (P : A Prop) (z : A) Lemma rtc_ind_l (P : A Prop) (z : A)
...@@ -152,7 +152,7 @@ Section rtc. ...@@ -152,7 +152,7 @@ Section rtc.
Global Instance: Transitive (tc R). Global Instance: Transitive (tc R).
Proof. exact tc_transitive. Qed. Proof. exact tc_transitive. Qed.
Lemma tc_r x y z : tc R x y R y z tc R x z. Lemma tc_r x y z : tc R x y R y z tc R x z.
Proof. intros. etransitivity; eauto. Qed. Proof. intros. etrans; eauto. Qed.
Lemma tc_rtc_l x y z : rtc R x y tc R y z tc R x z. Lemma tc_rtc_l x y z : rtc R x y tc R y z tc R x z.
Proof. induction 1; eauto. Qed. Proof. induction 1; eauto. Qed.
Lemma tc_rtc_r x y z : tc R x y rtc R y z tc R x z. Lemma tc_rtc_r x y z : tc R x y rtc R y z tc R x z.
......
...@@ -42,7 +42,7 @@ Proof. ...@@ -42,7 +42,7 @@ Proof.
split. split.
- now cofix; intros [??]; constructor. - now cofix; intros [??]; constructor.
- now cofix; intros ?? [??]; constructor. - now cofix; intros ?? [??]; constructor.
- cofix; intros ??? [??] [??]; constructor; etransitivity; eauto. - cofix; intros ??? [??] [??]; constructor; etrans; eauto.
Qed. Qed.
Global Instance scons_proper x : Proper (() ==> ()) (scons x). Global Instance scons_proper x : Proper (() ==> ()) (scons x).
Proof. by constructor. Qed. Proof. by constructor. Qed.
......
...@@ -54,6 +54,10 @@ Ltac done := ...@@ -54,6 +54,10 @@ Ltac done :=
Tactic Notation "by" tactic(tac) := Tactic Notation "by" tactic(tac) :=
tac; done. tac; done.
(** Aliases for trans and etrans that are easier to type *)
Tactic Notation "trans" constr(A) := transitivity A.
Tactic Notation "etrans" := etransitivity.
(** Tactics for splitting conjunctions: (** Tactics for splitting conjunctions:
- [split_and] : split the goal if is syntactically of the shape [_ ∧ _] - [split_and] : split the goal if is syntactically of the shape [_ ∧ _]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment