Commit d12478d2 authored by Ralf Jung's avatar Ralf Jung

prelude: missing lemmas about inj2; deduce list equality from list encoding

parent 2f8fd311
...@@ -899,6 +899,12 @@ Instance: RightAbsorb (↔) True impl. ...@@ -899,6 +899,12 @@ Instance: RightAbsorb (↔) True impl.
Proof. unfold impl. red; intuition. Qed. Proof. unfold impl. red; intuition. Qed.
Lemma not_inj `{Inj A B R R' f} x y : ¬R x y ¬R' (f x) (f y). Lemma not_inj `{Inj A B R R' f} x y : ¬R x y ¬R' (f x) (f y).
Proof. intuition. Qed. Proof. intuition. Qed.
Lemma not_inj2_1 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 :
¬R x1 x2 ¬R'' (f x1 y1) (f x2 y2).
Proof. intros HR HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
Lemma not_inj2_2 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 :
¬R' y1 y2 ¬R'' (f x1 y1) (f x2 y2).
Proof. intros HR' HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
Instance inj_compose {A B C} R1 R2 R3 (f : A B) (g : B C) : Instance inj_compose {A B C} R1 R2 R3 (f : A B) (g : B C) :
Inj R1 R2 f Inj R2 R3 g Inj R1 R3 (g f). Inj R1 R2 f Inj R2 R3 g Inj R1 R3 (g f).
Proof. red; intuition. Qed. Proof. red; intuition. Qed.
......
...@@ -222,6 +222,26 @@ Proof. apply (list_encode_app' [_]). Qed. ...@@ -222,6 +222,26 @@ Proof. apply (list_encode_app' [_]). Qed.
Lemma list_encode_suffix `{Countable A} (l k : list A) : Lemma list_encode_suffix `{Countable A} (l k : list A) :
l `suffix_of` k q, encode k = q ++ encode l. l `suffix_of` k q, encode k = q ++ encode l.
Proof. intros [l' ->]; exists (encode l'); apply list_encode_app. Qed. Proof. intros [l' ->]; exists (encode l'); apply list_encode_app. Qed.
Section not_serious.
(* FIXME This can't be real... it doesn't figure out the "flip eq" instance?!? *)
Local Instance: Assoc (flip (=)) (++).
Proof. intros ?? p. by induction p; intros; f_equal'. Qed.
Lemma list_encode_suffix_eq `{Countable A} q1 q2 (l1 l2 : list A) :
length l1 = length l2 q1 ++ encode l1 = q2 ++ encode l2 l1 = l2.
Proof.
revert q1 q2 l2; induction l1 as [|a1 l1 IH]; intros ???;
destruct l2 as [|a2 l2]; simpl; try discriminate; [done|].
intros EQ. injection EQ. clear EQ. intros EQ.
rewrite !list_encode_cons. intros Hl.
rewrite !assoc in Hl; eauto with typeclass_instances.
assert (l1 = l2) as EQl. { eapply IH; done. }
subst l2. apply (inj (++ (encode l1))) in Hl.
cut (a1 = a2); [congruence|]. apply (inj encode_nat).
revert Hl. clear.
generalize (encode_nat a2).
induction (encode_nat a1); intros [|?] ?; f_equal'; naive_solver.
Qed.
End not_serious.
(** ** Numbers *) (** ** Numbers *)
Instance pos_countable : Countable positive := Instance pos_countable : Countable positive :=
......
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