From 48ba6c006c966227b8a0b96ed48203af36835615 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 22:54:21 +0200 Subject: gmap2_idem --- lib/HashedMap.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'lib') diff --git a/lib/HashedMap.v b/lib/HashedMap.v index 1baff1a1..21f35af8 100644 --- a/lib/HashedMap.v +++ b/lib/HashedMap.v @@ -384,3 +384,19 @@ Section MAP2_IDEM. end end. + Lemma gmap2_idem: forall a b i, + get i (map2_idem a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { rewrite gmap2_idem_Empty. + rewrite gempty. + reflexivity. } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. -- cgit