From ff35e4e454150923bd45e4e034924e37f6644b06 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 14 Dec 2016 19:18:21 +0100
Subject: [PATCH] sum respects eqtype
---
theories/typing/sum.v | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index dbdb08b5..02c67710 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -107,6 +107,17 @@ Section sum.
iDestruct "Hlen" as %<-. done.
Qed.
+ Global Instance sum_proper E L:
+ Proper (Forall2 (eqtype E L) ==> eqtype E L) sum.
+ Proof.
+ (* TODO: Isn't there sth. showing that Forall2 is monotnous wrt. the predicate? *)
+ intros tyl1 tyl2 Heq.
+ assert (Forall2 (subtype E L) tyl1 tyl2 ∧ Forall2 (subtype E L) tyl2 tyl1).
+ { induction Heq as [|???? Heq]; first done. destruct_and!.
+ destruct Heq. split; constructor; done. }
+ destruct_and!. split; apply sum_mono; done.
+ Qed.
+
(* TODO : Make the Forall parameter a typeclass *)
(* TODO : This next step is suspuciously slow. *)
Global Instance sum_copy tyl :
--
GitLab