Commit 80572367 authored by Ralf Jung's avatar Ralf Jung
Browse files

per-fun refl is enough

parent 85a73e08
......@@ -15,7 +15,7 @@ Proof.
rewrite lookup_insert_ne //.
Qed.
Lemma sim_prog_sim_classical
Theorem sim_prog_sim_classical
prog_src
prog_tgt
`{NSD: stuck_decidable_1 prog_src}
......
......@@ -3,7 +3,16 @@ From stbor.sim Require Import refl_step.
Set Default Proof Using "Type".
Theorem sim_mod_fun_refl f :
⊨ᶠ f f.
Proof.
Admitted.
Lemma sim_mod_funs_refl prog :
sim_mod_funs prog prog.
Proof.
Admitted.
induction prog using map_ind.
{ intros ??. rewrite lookup_empty. done. }
apply sim_mod_funs_insert; try done.
apply sim_mod_fun_refl.
Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment