Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

complete proof that eval -> interpret #4

Merged
merged 6 commits into from
Jun 7, 2023
Merged

complete proof that eval -> interpret #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
e8ba551
add caml types
tabareau Jun 2, 2023
12c3e1d
fix after rebase
tabareau Jun 2, 2023
08fa00f
finish eval -> interpret
tabareau Jun 6, 2023
61474a0
fix after rebase
tabareau Jun 7, 2023
0d74f8f
refactoring
tabareau Jun 7, 2023
2058842
fix after refactoring
tabareau Jun 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ theories/Ceres/CeresFormat.v
theories/Ceres/CeresSerialize.v

theories/Malfunction.v
theories/utils_array.v
theories/SemanticsSpec.v
theories/Interpreter.v

Expand Down
18 changes: 10 additions & 8 deletions theories/CompileCorrect.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Local Open Scope string_scope.
From Malfunction Require Import Mcase.
From MetaCoq Require Import ReflectEq EWcbvEvalNamed bytestring MCList.

From Malfunction Require Import Compile SemanticsSpec.
From Malfunction Require Import Compile SemanticsSpec utils_array.

From Equations Require Import Equations.

Expand Down Expand Up @@ -291,8 +291,10 @@ Lemma eval_num `{Heap} Σ Γ_ i z h :
Proof.
intros. subst.
pose proof (Malfunction.Int63.of_Z_spec z) as Heq.
rewrite Zdiv.Zmod_small in Heq. rewrite <- Heq at 2.
Admitted.
rewrite Zdiv.Zmod_small in Heq; [| lia_max_length]. rewrite <- Heq at 2.
econstructor.
Qed.

(* todo "missing eval_num"%bs. eauto.
Qed.
*)
Expand All @@ -303,7 +305,7 @@ Lemma find_add_self {Hp : Heap} idx d na recs locals :
Malfunction.Ident.Map.find na (add_self (map fst recs) (RFunc_build (map snd recs)) locals)
= RClos (locals, map fst recs, RFunc_build (map snd recs), idx).
Proof.
intros Hdup Hnth. unfold add_self, add_recs, mapi.
intros Hdup Hnth. unfold add_self, add_recs, List.mapi.
unfold Malfunction.Ident.Map.find.
revert Hnth Hdup.
change idx with (0 + idx) at 2.
Expand All @@ -313,7 +315,7 @@ Proof.
- cbn. destruct a as [na' e].
destruct idx; cbn in Hnth; inversion Hnth.
+ subst. unfold Malfunction.Ident.Map.add, Malfunction.Ident.eqb.
rewrite eqb_refl. repeat f_equal. lia.
rewrite eqb_refl. repeat f_equal. lia.
+ unfold Malfunction.Ident.Map.add, Malfunction.Ident.eqb.
cbn. destruct (eqb_spec na na').
* subst. exfalso. inversion Hdup; subst. eapply H2.
Expand All @@ -328,7 +330,7 @@ Proof.
unfold fix_env. induction #|mfix| in idx |- *; cbn.
- lia.
- intros. destruct idx.
+ cbn. now rewrite <- minus_n_O.
+ cbn. now rewrite Nat.sub_0_r.
+ cbn. eapply IHn. lia.
Qed.

Expand Down Expand Up @@ -373,7 +375,7 @@ Proof.
- eauto.
+ pose proof (find_none _ _ E). cbn in *.
rewrite <- Hlocals. clear E.
unfold add_self, add_recs, mapi. generalize 0.
unfold add_self, add_recs, List.mapi. generalize 0.
generalize (RFunc_build (map snd recs)).
generalize (map fst recs) at 1.
assert (forall x, In x (map fst mfix) -> na <> x). {
Expand All @@ -383,7 +385,7 @@ Proof.
destruct (eqb_spec x x); try congruence. clear - H0.
unfold fix_env. generalize mfix at 2. induction mfix using rev_ind; cbn in *; eauto; intros.
rewrite map_app, in_app_iff in H0. cbn in H0.
rewrite app_length. cbn. rewrite plus_comm. cbn. rewrite map_app. cbn.
rewrite app_length. cbn. rewrite Nat.add_comm. cbn. rewrite map_app. cbn.
rewrite rev_app_distr. cbn.
destruct H0 as [ | [ | []]].
- edestruct IHmfix; eauto.
Expand Down
Loading