Commit 882fdc9d by Robbert Krebbers

### Remove FIXME in list_encode_suffix_eq.

parent d12478d2
 ... @@ -222,26 +222,17 @@ Proof. apply (list_encode_app' [_]). Qed. ... @@ -222,26 +222,17 @@ 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) : 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. length l1 = length l2 → q1 ++ encode l1 = q2 ++ encode l2 → l1 = l2. Proof. Proof. revert q1 q2 l2; induction l1 as [|a1 l1 IH]; intros ???; revert q1 q2 l2; induction l1 as [|a1 l1 IH]; destruct l2 as [|a2 l2]; simpl; try discriminate; [done|]. intros q1 q2 [|a2 l2] ?; simplify_equality'; auto. intros EQ. injection EQ. clear EQ. intros EQ. rewrite !list_encode_cons, !(assoc _); intros Hl. rewrite !list_encode_cons. intros Hl. assert (l1 = l2) as <- by eauto; clear IH; f_equal. rewrite !assoc in Hl; eauto with typeclass_instances. apply (inj encode_nat); apply (inj (++ encode l1)) in Hl; revert Hl; clear. assert (l1 = l2) as EQl. { eapply IH; done. } generalize (encode_nat a2). subst l2. apply (inj (++ (encode l1))) in Hl. induction (encode_nat a1); intros [|?] ?; naive_solver. 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. 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