From 0892b99d00aac6ad9f7467f1383fe5dc1b45e94f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 10 Mar 2020 09:45:34 +0100 Subject: eq_find_sound --- backend/CSE3analysisproof.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'backend/CSE3analysisproof.v') diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 027a874a..4fa093c6 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -373,4 +373,20 @@ Section SOUNDNESS. Qed. Hint Resolve kill_mem_sound : cse3. + + Theorem eq_find_sound: + forall no eq id, + eq_find (ctx := ctx) no eq = Some id -> + eq_catalog ctx id = Some eq. + Proof. + unfold eq_find. + intros. + destruct (eq_find_oracle ctx no eq) as [ id' | ]. + 2: discriminate. + destruct (eq_catalog ctx id') as [eq' |] eqn:CATALOG. + 2: discriminate. + destruct (eq_dec_equation eq eq'). + 2: discriminate. + congruence. + Qed. End SOUNDNESS. -- cgit