From 5ffa8534d09272e5f44c51193e74cffdbc2b043c Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 7 Oct 2019 15:44:20 +0200 Subject: Icond --- backend/Duplicateproof.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'backend/Duplicateproof.v') diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index aa605bea..ba1fecc1 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -127,6 +127,15 @@ Proof. destruct (builtin_res_eq_pos _ _); try discriminate. eapply verify_is_copy_correct_one. destruct x. eassumption. subst. constructor. +(* Icond *) + - destruct i'; try (inversion H; fail). monadInv H. + unfold verify_is_copy in EQ, EQ1. + destruct (_ ! n1) eqn:REVM; [|inversion EQ]. + destruct (n ?= p) eqn:NP; try (inversion EQ; fail). eapply Pos.compare_eq in NP. subst. inv EQ. + destruct (_ ! n2) eqn:REVMM; [|inversion EQ1]. + destruct (n0 ?= p0) eqn:NP0; try (inversion EQ1; fail). eapply Pos.compare_eq in NP0. subst. inv EQ1. + destruct (condition_eq _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. constructor; assumption. (* Ireturn *) - destruct i'; try (inversion H; fail). destruct (option_eq _ _ _); try discriminate. subst. clear H. -- cgit