diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-16 22:54:21 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-16 22:54:21 +0200 |
| commit | 48ba6c006c966227b8a0b96ed48203af36835615 (patch) | |
| tree | 73629ad072958d0f096c2c950d26465aabf05093 /lib | |
| parent | 0575b91176870ac5d1c5692d19059a12e4d9667c (diff) | |
| download | compcert-kvx-48ba6c006c966227b8a0b96ed48203af36835615.tar.gz compcert-kvx-48ba6c006c966227b8a0b96ed48203af36835615.zip | |
gmap2_idem
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/HashedMap.v | 16 |
1 files changed, 16 insertions, 0 deletions
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. |