Commit 7d197b3e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Break at 80

parent a07cc19d
...@@ -2283,7 +2283,8 @@ Section Forall2. ...@@ -2283,7 +2283,8 @@ Section Forall2.
Proof. Proof.
intro. unfold sublist_lookup, sublist_alter. intro. unfold sublist_lookup, sublist_alter.
erewrite <-Forall2_length by eauto; intros; simplify_option_equality. erewrite <-Forall2_length by eauto; intros; simplify_option_equality.
apply Forall2_app_l; rewrite ?take_length_le by lia; auto using Forall2_take. apply Forall2_app_l;
rewrite ?take_length_le by lia; auto using Forall2_take.
apply Forall2_app_l; erewrite Forall2_length, take_length, apply Forall2_app_l; erewrite Forall2_length, take_length,
drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|]. drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|].
rewrite drop_drop; auto using Forall2_drop. rewrite drop_drop; auto using Forall2_drop.
......
...@@ -48,12 +48,7 @@ Qed. ...@@ -48,12 +48,7 @@ Qed.
Global Instance listset_nodup_elems: Elements A C := listset_nodup_car. Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
Global Instance: FinCollection A C. Global Instance: FinCollection A C.
Proof. Proof. split. apply _. done. by intros [??]. Qed.
split.
* apply _.
* done.
* by intros [??].
Qed.
Global Instance: CollectionOps A C. Global Instance: CollectionOps A C.
Proof. Proof.
split. split.
......
...@@ -9,24 +9,20 @@ Instance: ProofIrrel True. ...@@ -9,24 +9,20 @@ Instance: ProofIrrel True.
Proof. by intros [] []. Qed. Proof. by intros [] []. Qed.
Instance: ProofIrrel False. Instance: ProofIrrel False.
Proof. by intros []. Qed. Proof. by intros []. Qed.
Instance and_pi (A B : Prop) : Instance and_pi (A B : Prop) :
ProofIrrel A ProofIrrel B ProofIrrel (A B). ProofIrrel A ProofIrrel B ProofIrrel (A B).
Proof. intros ?? [??] [??]. by f_equal. Qed. Proof. intros ?? [??] [??]. by f_equal. Qed.
Instance prod_pi (A B : Type) : Instance prod_pi (A B : Type) :
ProofIrrel A ProofIrrel B ProofIrrel (A * B). ProofIrrel A ProofIrrel B ProofIrrel (A * B).
Proof. intros ?? [??] [??]. by f_equal. Qed. Proof. intros ?? [??] [??]. by f_equal. Qed.
Instance eq_pi {A} `{ x y : A, Decision (x = y)} (x y : A) : Instance eq_pi {A} `{ x y : A, Decision (x = y)} (x y : A) :
ProofIrrel (x = y). ProofIrrel (x = y).
Proof. Proof.
intros ??. apply eq_proofs_unicity. intros ??. apply eq_proofs_unicity.
intros x' y'. destruct (decide (x' = y')); tauto. intros x' y'. destruct (decide (x' = y')); tauto.
Qed. Qed.
Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b). Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b).
Proof. destruct b; simpl; apply _. Qed. Proof. destruct b; simpl; apply _. Qed.
Lemma sig_eq_pi `(P : A Prop) `{ x, ProofIrrel (P x)} Lemma sig_eq_pi `(P : A Prop) `{ x, ProofIrrel (P x)}
(x y : sig P) : x = y `x = `y. (x y : sig P) : x = y `x = `y.
Proof. Proof.
...@@ -34,7 +30,6 @@ Proof. ...@@ -34,7 +30,6 @@ Proof.
destruct x as [x Hx], y as [y Hy]; simpl; intros; subst. destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
f_equal. apply proof_irrel. f_equal. apply proof_irrel.
Qed. Qed.
Lemma exists_proj1_pi `(P : A Prop) `{ x, ProofIrrel (P x)} Lemma exists_proj1_pi `(P : A Prop) `{ x, ProofIrrel (P x)}
(x : sig P) p : `x p = x. (x : sig P) p : `x p = x.
Proof. by apply (sig_eq_pi _). Qed. Proof. by apply (sig_eq_pi _). Qed.
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