Switch `inj _` to `inj f`, part 2

Code not affected by a00d9bd8.

All occurrences are gone, except for one in `base.v` where you'd need different
functions.

However, I'm unsure this is an improvement: in lots of cases here, the function
didn't need to be guessed, but could be deduced by "simple" higher-order
unification, the one where unifying `?f ?a` against `g args last_arg` sets `?f =
g args`.
parent ba2bdb73
......@@ -222,7 +222,7 @@ Proof.
rewrite !multiplicity_disj_union. lia.
Qed.
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (. X).
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj (X .)). Qed.
Lemma gmultiset_disj_union_intersection_l X Y Z : X (Y Z) = (X Y) (X Z).
Proof.
......
......@@ -2232,7 +2232,7 @@ Qed.
Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 ⊆+ k ++ l2 → l1 ⊆+ l2.
Proof.
induction k as [|y k IH]; simpl; [done |]. rewrite submseteq_cons_l.
intros (?&E%(inj _)&?). apply IH. by rewrite E.
intros (?&E%(inj (cons y))&?). apply IH. by rewrite E.
Qed.
Lemma submseteq_app_inv_r l1 l2 k : l1 ++ k ⊆+ l2 ++ k → l1 ⊆+ l2.
Proof.
......
......@@ -710,7 +710,7 @@ Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
Instance Qp_plus_comm : Comm (=) Qp_plus.
Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed.
Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p).
Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj _). Qed.
Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). Qed.
Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp.
Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed.
......@@ -794,9 +794,9 @@ Proof.
destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq].
- auto.
- destruct (help c d a b); [done..|]. naive_solver.
- apply (inj _) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
- apply (inj (Qp_plus a)) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
eauto 10 using (comm_L Qp_plus). }
intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj _).
intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)).
destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
eexists a', q, (q + e)%Qp, d'; split_and?; auto using (comm_L Qp_plus).
- by rewrite (assoc_L _), (comm_L Qp_plus e).
......
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