Commit 772ff880 authored by Dan Frumin's avatar Dan Frumin

Prove `dcexpr_interp_mono`.

parent f002e839
......@@ -361,15 +361,18 @@ Proof.
Qed.
Lemma dcexpr_interp_mono (X: list string) (E E': known_locs) (de: dcexpr) :
dcexpr_wf X E de E `prefix_of` E' dcexpr_interp E de = dcexpr_interp E' de.
dcexpr_wf X E de E `prefix_of` E'
dcexpr_interp E de = dcexpr_interp E' de.
Proof.
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) ||
(apply andb_prop_elim in H as [H1 H2];
rewrite IHde2; [rewrite IHde1; done | done | done ];
by rewrite (IHde1 H1 Hpre (dcexpr_interp E de1))) || eauto.
by rewrite (dexpr_interp_mono X E E').
Admitted.
revert X.
induction de; simplify_eq /=; intros X H Hpre; eauto;
destruct_and?;
try by rewrite (IHde X)
|| (rewrite (IHde2 X) // (IHde1 X) //).
- by rewrite (dexpr_interp_mono X E E').
- rewrite (IHde1 X) //.
by erewrite (IHde2 (_::X)).
Qed.
Global Instance dexpr_closed X E de :
dexpr_wf X E de
......
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