(****************************************************************
Copyright © 2007-2024 Amy Felty
This file is part of "Two-Level Hybrid in Coq"
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see .
***************************************************************)
(****************************************************************
File: SR_MiniML_eval.v
original: July 2007
updated: February 2015
Apr 2024: Current Coq Version: V8.18.0
Subject Reduction for Call-by-Value Mini-ML using Hybrid
Example from:
[1] Amy Felty and Alberto Momigliano, Hybrid: A Definitional Two Level
Approach to Reasoning with Higher-Order Abstract Syntax, In Journal
of Automated Reasoning, 48(1):43-105, 2012.
***************************************************************)
From HybridSys Require Export sl.
From HybridSys Require Export MiniML.
(****************************************************************
****************************************************************
The two-level encoding of isterm, eval, and hastype judgments
as in Figure 6 in [1].
****************************************************************
****************************************************************)
(****************************************************************
The atm type and instantiation of oo.
****************************************************************)
Section encoding.
Inductive atm : Set :=
typeof : uexp -> tp -> atm
| eval : uexp -> uexp -> atm
| isterm : uexp -> atm.
Definition oo_ := oo atm Econ.
Definition atom_ : atm -> oo_ := atom Econ.
Definition T_ : oo_ := T atm Econ.
Hint Unfold oo_ atom_ T_: hybrid.
(****************************************************************
Definition of prog
****************************************************************)
Inductive prog : atm -> oo_ -> Prop :=
| tabs :
forall (T1 T2: tp) (E : uexp -> uexp),
abstr E ->
prog (typeof (Fun (fun x => E x)) (arrow T1 T2))
(All (fun x : uexp => Imp (typeof x T1) (atom_ (typeof (E x) T2))))
| tap :
forall E1 E2: uexp, forall T T' : tp,
prog (typeof (App E1 E2) T)
(Conj (atom_ (typeof E1 (arrow T' T))) (atom_ (typeof E2 T')))
| tfix :
forall (T: tp) (E : uexp -> uexp),
abstr E ->
prog (typeof (Fix (fun x => E x)) T)
(All (fun x : uexp => Imp (typeof x T) (atom_ (typeof (E x) T))))
| eap : forall E1':uexp -> uexp, forall E1 E2 V V2:uexp,
abstr E1' ->
prog (eval (App E1 E2) V)
(Conj (atom_ (eval E1 (Fun (fun x => E1' x))))
(Conj (atom_ (eval E2 V2))
(atom_ (eval (E1' V2) V))))
| eabs : forall E:uexp -> uexp, (abstr E) ->
prog (eval (Fun (fun x => E x)) (Fun (fun x => E x)))
(atom_ (isterm (Fun (fun x => E x))))
| efix : forall E:uexp -> uexp, forall V:uexp,
abstr E ->
prog (eval (Fix (fun x => E x)) V)
(Conj (atom_ (eval (E (Fix (fun x => E x))) V))
(atom_ (isterm (Fix (fun x => E x)))))
| exp_app : forall M N:uexp,
prog (isterm (App M N))
(Conj (atom_ (isterm M)) (atom_ (isterm N)))
| exp_lam : forall (E:uexp -> uexp),
abstr E ->
prog (isterm (Fun (fun x => (E x))))
(All (fun x:uexp => (Imp (isterm x) (atom_ (isterm (E x))))))
| exp_fix : forall (E:uexp -> uexp),
abstr E ->
prog (isterm (Fix (fun x => (E x))))
(All (fun x:uexp => (Imp (isterm x) (atom_ (isterm (E x)))))).
(****************************************************************
Instantiation of seq
****************************************************************)
Definition seq_ : nat -> list atm -> oo_ -> Prop := sl.seq prog.
Definition seq'_ := seq' prog.
Definition seq0 (B : oo_) : Prop := seq'_ nil B.
End encoding.
#[global] Hint Unfold oo_ atom_ T_: hybrid.
#[global] Hint Unfold seq_ seq'_ seq0: hybrid.
#[global] Hint Unfold proper: hybrid.
#[global] Hint Resolve proper_Var : hybrid.
#[global] Hint Resolve tabs tap tfix eap eabs efix exp_app exp_lam exp_fix : hybrid.
(************************)
(* Inversion Properties *)
(************************)
(* Specialized inversion properties of prog (could be automated) *)
Section prog_inv.
Lemma typeof_abs_inv :
forall (i:nat) (l:list atm) (T T':tp) (E:uexp->uexp),
(forall x : uexp,
proper x ->
seq_ i l (Imp (typeof x T) (atom_ (typeof (E x) T')))) ->
exists j:nat, (i=j+1 /\
forall x : uexp,
proper x ->
seq_ j ((typeof x T)::l) (atom_ (typeof (E x) T'))).
Proof.
induction i; auto.
- intros l T T' E H.
generalize (H (Var 0) (proper_Var 0)); intro H1.
inversion H1; clear H1; subst.
replace (i+1) with (S i) in H0; try lia.
- intros l T T' E H.
clear IHi.
exists i; split; try lia.
intros x H0.
generalize (H x H0); intro H1.
inversion H1; clear H1; subst.
assert (i0 = i); try lia.
subst; auto.
Qed.
End prog_inv.
(****************************************************************
****************************************************************
Version of internal adequacy and subject reduction with eval
judgments defined using the specification logic as described in
Section 4.2 of [1]
****************************************************************
****************************************************************)
(****************************************************************
Adequacy: proper conditions
****************************************************************)
Section proper_adeq.
Lemma eval_proper_l : forall E V:uexp,
seq0 (atom_ (eval E V)) -> (proper E).
Proof.
intros E V [n h1].
generalize E V h1; clear h1 E V.
generalize
(lt_wf_ind n
(fun n:nat =>
forall E V : uexp, seq_ n nil (atom_ (eval E V)) -> proper E)).
intro h'.
apply h'; clear h'; auto.
clear n.
intros n h1 E V h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
- inversion H3; clear H3; subst.
inversion H6; clear H6; subst.
assert (i E1' x)) H5); intro h3.
apply proper_App; auto.
- apply proper_Fun; auto.
- apply proper_Fix; auto.
Qed.
Lemma eval_proper_r : forall E V:uexp,
seq0 (atom_ (eval E V)) -> (proper V).
intros E V [n h1].
generalize E V h1; clear h1 E V.
generalize
(lt_wf_ind n
(fun n:nat =>
forall E V : uexp, seq_ n nil (atom_ (eval E V)) -> proper V)).
intro h'.
apply h'; clear h'; auto.
clear n.
intros n h1 E V h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
- inversion H3; clear H3; subst.
inversion H6; clear H6; subst.
apply h1 with i (E1' V2); auto; lia.
- apply proper_Fun; auto.
- inversion H3; clear H3; subst.
apply h1 with i0 (E0 (Fix (fun x : uexp => E0 x))); auto; lia.
Qed.
(* MC-Lemma 20 (1) from [1] *)
Lemma eval_proper : forall E V:uexp,
seq0 (atom_ (eval E V)) -> (proper E) /\ (proper V).
Proof.
intros E V h1; split.
- apply eval_proper_l with V; auto.
- apply eval_proper_r with E; auto.
Qed.
(* MC-Lemma 20 (3) from [1] *)
Lemma hastype_proper : forall (E:uexp) (T:tp),
seq0 (atom_ (typeof E T)) -> (proper E).
Proof.
intros E T [n h1].
generalize E T h1; clear h1 E T.
generalize
(lt_wf_ind n
(fun n:nat =>
forall (E : uexp) (T : tp), seq_ n nil (atom_ (typeof E T)) -> proper E)).
intro h'.
apply h'; clear h'; auto.
clear n.
intros n h1 E T h2.
inversion h2; clear h2; subst.
inversion H0; clear H0; subst.
- apply proper_Fun; auto.
- inversion H3; clear H3; subst.
apply proper_App; auto.
+ apply h1 with i0 (arrow T' T); auto; try lia.
+ apply h1 with i0 T'; auto; try lia.
- apply proper_Fix; auto.
Qed.
End proper_adeq.
(****************************************************************
Internal Adequacy of Judgments
****************************************************************)
Section adeq.
Inductive txR: list atm -> list atm -> Prop :=
| nil_tx: txR nil nil
| cons_tx: forall (Phi Psi:list atm) (x:uexp) (T:tp), proper x ->
txR Phi Psi ->
txR (typeof x T::Phi) (isterm x::Psi).
Hint Resolve nil_tx cons_tx : hybrid.
Lemma memb_tx : forall (Phi Psi:list atm) (x:uexp) (T:tp),
txR Phi Psi -> In (typeof x T) Phi -> In (isterm x) Psi.
Proof.
intros Phi Psi x; induction 1; eauto with hybrid.
intro h2; simpl in h2; destruct h2 as [h2 | h2].
- injection h2; intros; subst; simpl; auto.
- simpl; tauto.
Qed.
Lemma hastype_isterm_ctx :
forall (i:nat) (M:uexp) (T:tp) (l l':list atm),
txR l l' ->
seq_ i l (atom_ (typeof M T)) ->
seq_ i l' (atom_ (isterm M)).
Proof.
intro i.
generalize
(lt_wf_ind i
(fun i:nat =>
forall (M : uexp) (T : tp) (l l' : list atm),
txR l l' ->
seq_ i l (atom_ (typeof M T)) -> seq_ i l' (atom_ (isterm M)))).
intro H'.
apply H'; clear H' i; auto.
intros i h M T l l' h1 h2.
inversion h2; subst; clear h2.
- inversion H0; subst; clear H0.
(* Fun case *)
+ inversion H3; subst; clear H3.
generalize (typeof_abs_inv i l T1 T2 E H2); clear H2; intros [j [h3 h4]];
subst.
unfold seq_,atom_;
apply s_bc with
(All (fun x:uexp => (Imp (isterm x) (atom_ (isterm (E x)))))).
* apply exp_lam; auto.
* apply s_all; auto.
intros x h5.
apply s_imp; auto.
apply h with T2 (typeof x T1::l); eauto with hybrid.
lia.
(* App case *)
+ inversion H3; subst; clear H3.
unfold seq_,atom_; apply s_bc with (Conj (atom_ (isterm E1)) (atom_ (isterm E2))).
* apply exp_app.
* apply s_and; auto.
apply h with (arrow T' T) l; auto.
lia.
apply h with T' l; auto.
lia.
(* Fix case *)
+ inversion H3; subst; clear H3.
generalize (typeof_abs_inv i l T T E H2); clear H2; intros [j [h3 h4]];
subst.
unfold seq_,atom_;
apply s_bc with
(All (fun x:uexp => (Imp (isterm x) (atom_ (isterm (E x)))))).
* apply exp_fix; auto.
* apply s_all; auto.
intros x h5.
apply s_imp; auto.
apply h with T (typeof x T::l); eauto with hybrid.
lia.
(* context case *)
- specialize memb_tx with (1:=h1) (2:=H2).
case l'.
+ simpl; tauto.
+ intros a l'' h2; unfold seq_,atom_; apply s_init; auto.
Qed.
(* MC-Lemma 20 (4) from [1] *)
Lemma hastype_isterm : forall (M:uexp) (T:tp),
seq0 (atom_ (typeof M T)) ->
seq0 (atom_ (isterm M)).
Proof.
intros M T [i h].
generalize nil_tx; intro h1.
generalize (hastype_isterm_ctx i M T nil nil); intro h2.
exists i; tauto.
Qed.
Lemma eval_isterm_ctx : forall (i:nat) (M N:uexp),
seq_ i nil (atom_ (eval M N)) ->
(seq_ i nil (atom_ (isterm M)) /\ seq_ i nil (atom_ (isterm N))).
Proof.
intro i.
generalize
(lt_wf_ind i
(fun i:nat =>
forall M N : uexp,
seq_ i nil (atom_ (eval M N)) ->
seq_ i nil (atom_ (isterm M)) /\ seq_ i nil (atom_ (isterm N)))).
intro H'; apply H'; clear H' i; auto.
intros i h M N h3.
inversion h3; subst; clear h3.
inversion H0; subst; clear H0.
- inversion H3; subst; clear H3.
inversion H6; subst; clear H6.
(* App case *)
+ assert (ha1: (i0
(seq0 (atom_ (isterm M)) /\ seq0 (atom_ (isterm N))).
Proof.
intros M N [i h].
specialize eval_isterm_ctx with (1:=h); intros [h1 h2].
split; exists i; auto.
Qed.
End adeq.
(****************************************************************
Subject Reduction (Type Soundness)
****************************************************************)
Section sr.
(* MC-Theorem 24 from [1] *)
Theorem OL_subject_reduction :
forall e v : uexp, seq0 (atom_ (eval e v)) ->
forall t : tp, seq0 (atom_ (typeof e t)) -> seq0 (atom_ (typeof v t)).
intros e v H t H0.
unfold seq0 in H; elim H; clear H; intros n H.
generalize
(lt_wf_ind n
(fun j:nat =>
forall e v:uexp, seq_ j nil (atom_ (eval e v)) ->
forall t:tp, seq0 (atom_ (typeof e t)) ->
seq0 (atom_ (typeof v t)))).
intro H'.
apply H' with e; clear H'; auto.
clear H n H0 e v t.
intros n H e v H0 t H1.
inversion H0; clear H0; subst.
inversion H3; clear H3; subst.
(* App case *)
- inversion H6; clear H6; subst.
inversion H8; clear H8; subst.
unfold seq0 in H1; elim H1; clear H1; intros j H1.
inversion H1; clear H1; subst.
inversion H2; clear H2; subst.
inversion H8; clear H8; subst.
assert (seq0 (atom_ (typeof E1 (arrow T' t)))).
{ unfold seq0,seq_; exists i1; auto. }
assert (seq0 (atom_ (typeof E2 T'))).
{ unfold seq0,seq_; exists i1; auto. }
clear H4 H10.
assert (i < i+1+1+1); try lia.
assert (i+1 < i+1+1+1); try lia.
generalize (H i H2 E2 V2 H6 T' H1); intro H4.
generalize (H (i+1) H3 E1 (Fun (fun x => E1' x)) H7 (arrow T' t) H0);
intro H8.
unfold seq0 in H8.
elim H8; clear H8; intros j H8.
inversion H8; clear H8; subst.
inversion H11; clear H11; subst.
inversion H14; clear H14; subst.
generalize (typeof_abs_inv i2 nil T' t E H13); intro H10.
elim H10; clear H10; intros j [Heq H10].
subst.
clear H13.
assert (proper V2).
{ apply eval_proper_r with E2.
unfold seq0; exists i; auto. }
generalize (H10 V2 H11); clear H10; intro H10.
generalize (abstr_eta H15); intro H15'.
generalize (abstr_eta H5); intro H5'.
generalize (abstr_lbind_simp H15' H5' H8); intro H12.
unfold ext_eq in H12.
rewrite H12 in H10; auto; clear H12 H15' H8 H15 E.
apply H with i (E1' V2); auto; try lia.
unfold seq0, seq_.
apply seq_cut with (typeof V2 T'); auto.
unfold seq'.
exists j; auto.
(* Fun case *)
- exact H1.
(* Fix case *)
- elim H1; intros j H1'.
inversion H1'; clear H1'; subst.
inversion H2; clear H2; subst.
inversion H7; clear H7; subst.
generalize (typeof_abs_inv i1 nil t t E0 H9); clear H9; intro H9.
elim H9; clear H9; intros j [Heq H9]; subst.
generalize (H9 (Fix (fun x : uexp => E x))); clear H9; intro H9.
generalize (abstr_eta H5); intro H5'.
generalize (abstr_eta H8); intro H8'.
generalize (abstr_lbind_simp H8' H5' H0); intro H1'.
unfold ext_eq in H1'.
rewrite -> H1' in H9; auto.
+ clear H1' H8' H0 H8 E0.
generalize (abstr_proper_Fix (fun x => E x) H5'); intro H0.
generalize (H9 H0); clear H9; intro H9.
inversion H6; subst; clear H6.
apply H with i0 (E (Fix (fun x : uexp => E x))); auto; try lia.
unfold seq0, seq_.
apply seq_cut with (typeof (Fix (fun x : uexp => E x)) t); auto.
unfold seq'.
exists j; auto.
+ apply proper_Fix; auto.
Qed.
End sr.
(****************************************************************
****************************************************************
Equivalence of eval and meval
****************************************************************
****************************************************************)
Section equiv.
(****************************************************************
Evaluation
****************************************************************)
Inductive meval: uexp -> uexp -> Prop :=
eval_App: forall E1':uexp -> uexp, forall E1 E2 V V2:uexp,
abstr E1' ->
meval E1 (Fun (fun x => E1' x)) ->
meval E2 V2 -> meval (E1' V2) V ->
meval (App E1 E2) V
| eval_Fun: forall E:uexp -> uexp, abstr E ->
seq0 (atom_ (isterm (Fun (fun x => E x)))) ->
meval (Fun (fun x => E x)) (Fun (fun x => E x))
| eval_Fix: forall E:uexp -> uexp, forall V:uexp,
abstr E ->
seq0 (atom_ (isterm (Fix (fun x => E x)))) ->
meval (E (Fix (fun x => E x))) V ->
meval (Fix (fun x => E x)) V.
(* MC-Theorem 25 from [1] *)
Theorem eval_equiv_meval : forall e v:uexp,
(meval e v) <-> seq0 (atom_ (eval e v)).
Proof.
intros e v; split.
(* -> *)
- induction 1; auto with hybrid.
(* App case *)
+ destruct IHmeval1 as [i1 h1].
destruct IHmeval2 as [i2 h2].
destruct IHmeval3 as [i3 h3].
exists (i1+i2+i3+1+1+1+1).
unfold seq_,atom_;
apply s_bc with
(Conj (atom_ (eval E1 (Fun (fun x => E1' x))))
(Conj (atom_ (eval E2 V2))
(atom_ (eval (E1' V2) V)))); eauto with hybrid.
apply s_and.
* apply seq_mono with i1; try lia; auto.
* apply s_and.
-- apply seq_mono with i2; try lia; auto.
-- apply seq_mono with i3; try lia; auto.
(* Fun case *)
+ destruct H0 as [i h].
exists (i+1).
unfold seq_,atom_; apply s_bc with (atom_ (isterm (Fun (fun x => E x))));
eauto with hybrid.
(* Fix case *)
+ destruct H0 as [i1 h1].
destruct IHmeval as [i2 h2].
exists (i1+i2+1+1+1).
unfold seq_,atom_;
apply s_bc with
(Conj (atom_ (eval (E (Fix (fun x => E x))) V))
(atom_ (isterm (Fix (fun x => E x))))); eauto with hybrid.
apply s_and; auto.
* apply seq_mono with i2; try lia; auto.
* apply seq_mono with i1; try lia; auto.
(* <- *)
- intro h.
unfold seq0 in h; elim h; clear h; intros n h.
generalize
(lt_wf_ind n
(fun j:nat =>
forall e v:uexp,
seq_ j nil (atom_ (eval e v)) -> meval e v)).
intro H'.
apply H'; clear H'; auto.
clear h n e v.
intros n H e v H0.
inversion H0; subst; clear H0.
inversion H2; subst; clear H2.
(* App case *)
+ inversion H5; subst; clear H5.
inversion H7; subst; clear H7.
apply eval_App with E1' V2; auto.
* apply H with (i+1); auto; try lia.
* apply H with i; auto; try lia.
* apply H with i; auto; try lia.
(* Fun case *)
+ apply eval_Fun; auto.
exists i; auto.
(* Fix case *)
+ inversion H5; subst; clear H5.
apply eval_Fix; auto.
* exists i0; auto.
* apply H with i0; auto; try lia.
Qed.
End equiv.