Coral.Interp: relational interpretation of untyped λ-terms
Require Import Infrastructure.
Import Notations.
Require Import Env.
Require Import Rel.
Require Import Transp.
Require Import SupportFacts.
Require Import RelExtra.
Require Import RelWf.
Require Import Rsem.
Require Import TermInd.
Require Import StepsFacts.
Require Import EvalFacts.
A denotational semantics of the lambda-calculus based on relations
that model their input/output behaviours. The definition expects the
term to be locally-closed (i.e. a wellformed term in the
locally-nameless representation), and expects that the environment
contains at least the free variables of the term. This is Figure 4 of
the ICFP'20 paper.
Definition Interp
(E: env (rel (env term) term)) (t: term)
(Hlc: lc t) (Hfv: fv t [<=] dom E)
: rel (env term) term :=
term_recurse
(fun E x E_x ⇒ (* Var *)
RelInter (RelSelf (Var x)) (RelGather E))
(fun E t1 R1 ⇒ R1) (* Let argument *)
(fun E t1 R1 x t2 R2 ⇒ (* Let *)
RelLet (dom E) x R1 R2)
(fun E ⇒ RelTopEnvVal) (* Lam argument *)
(fun E x t R ⇒ (* Lam *)
RelInter (RelLam (dom E) x RelTopEnvVal R)
(RelInter (RelSelf (Lam (close x t))) (RelGather E)))
(fun E t1 R1 t2 R2 ⇒ (* App *)
APP R1 R2)
(fun E ⇒ (* Unit *)
RelInter RelUnitR (RelGather E))
(fun E t1 R1 t2 R2 ⇒ (* Pair *)
RelPairR R1 R2)
(fun E t R ⇒ (* Fst *)
RelCompose R (RelPairL RelEqVal RelTopVal))
(fun E t R ⇒ (* Snd *)
RelCompose R (RelPairL RelTopVal RelEqVal))
(fun E t R ⇒ (* InjL *)
RelSumR R RelBot)
(fun E t R ⇒ (* InjR *)
RelSumR RelBot R)
(fun E t R ⇒ RelCompose R (RelSumL RelEqVal RelBot)) (* Match 1st argument *)
(fun E t R ⇒ RelCompose R (RelSumL RelBot RelEqVal)) (* Match 2nd argument *)
(fun E t R x1 t1 R1 x2 t2 R2 ⇒ (* Match *)
RelUnion
(RelLet (dom E) x1 (RelCompose R (RelSumL RelEqVal RelBot)) R1)
(RelLet (dom E) x2 (RelCompose R (RelSumL RelBot RelEqVal)) R2)
)
E t Hlc Hfv
.
(E: env (rel (env term) term)) (t: term)
(Hlc: lc t) (Hfv: fv t [<=] dom E)
: rel (env term) term :=
term_recurse
(fun E x E_x ⇒ (* Var *)
RelInter (RelSelf (Var x)) (RelGather E))
(fun E t1 R1 ⇒ R1) (* Let argument *)
(fun E t1 R1 x t2 R2 ⇒ (* Let *)
RelLet (dom E) x R1 R2)
(fun E ⇒ RelTopEnvVal) (* Lam argument *)
(fun E x t R ⇒ (* Lam *)
RelInter (RelLam (dom E) x RelTopEnvVal R)
(RelInter (RelSelf (Lam (close x t))) (RelGather E)))
(fun E t1 R1 t2 R2 ⇒ (* App *)
APP R1 R2)
(fun E ⇒ (* Unit *)
RelInter RelUnitR (RelGather E))
(fun E t1 R1 t2 R2 ⇒ (* Pair *)
RelPairR R1 R2)
(fun E t R ⇒ (* Fst *)
RelCompose R (RelPairL RelEqVal RelTopVal))
(fun E t R ⇒ (* Snd *)
RelCompose R (RelPairL RelTopVal RelEqVal))
(fun E t R ⇒ (* InjL *)
RelSumR R RelBot)
(fun E t R ⇒ (* InjR *)
RelSumR RelBot R)
(fun E t R ⇒ RelCompose R (RelSumL RelEqVal RelBot)) (* Match 1st argument *)
(fun E t R ⇒ RelCompose R (RelSumL RelBot RelEqVal)) (* Match 2nd argument *)
(fun E t R x1 t1 R1 x2 t2 R2 ⇒ (* Match *)
RelUnion
(RelLet (dom E) x1 (RelCompose R (RelSumL RelEqVal RelBot)) R1)
(RelLet (dom E) x2 (RelCompose R (RelSumL RelBot RelEqVal)) R2)
)
E t Hlc Hfv
.
Unfolding lemma, showing that we indeed have defined the intended function.
Lemma Interp_equations E t (Hlc: lc t) (Hfv: fv t [<=] dom E) :
match t with
| BVar _ ⇒ False
| Var x ⇒
∃ Rx, get x E = Some Rx ∧
Interp E t Hlc Hfv = RelInter (RelSelf (Var x)) (RelGather E)
| Let t1 t2 ⇒
∃ x (Hx: x `notin` dom E) t2' (Heq: t2 = close x t2')
(Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E)
(Hlc2: lc t2') (Hfv2: fv t2' [<=] add x (dom E)),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
let R2 := Interp (x ¬ R1 ++ E) t2' Hlc2 Hfv2 in
RelLet (dom E) x R1 R2
| Lam t1 ⇒
∃ x (Hx: x `notin` dom E) t1' (Heq: t1 = close x t1')
(Hlc1: lc t1') (Hfv1: fv t1' [<=] add x (dom E)),
Interp E t Hlc Hfv =
let R := Interp (x ¬ RelTopEnvVal ++ E) t1' Hlc1 Hfv1 in
RelInter (RelLam (dom E) x RelTopEnvVal R)
(RelInter (RelSelf (Lam (close x t1'))) (RelGather E))
| App t1 t2 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
let R2 := Interp E t2 Hlc2 Hfv2 in
APP R1 R2
| Unit ⇒
Interp E t Hlc Hfv = RelInter RelUnitR (RelGather E)
| Pair t1 t2 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
let R2 := Interp E t2 Hlc2 Hfv2 in
RelPairR R1 R2
| Fst t1 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
RelCompose R1 (RelPairL RelEqVal RelTopVal)
| Snd t1 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
RelCompose R1 (RelPairL RelTopVal RelEqVal)
| InjL t1 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
RelSumR R1 RelBot
| InjR t1 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
RelSumR RelBot R1
| Match t0 t1 t2 ⇒
∃ x1 (Hx1: x1 `notin` dom E) t1' (Heq: t1 = close x1 t1')
x2 (Hx2: x2 `notin` dom E) t2' (Heq: t2 = close x2 t2')
(Hlc0: lc t0) (Hfv0: fv t0 [<=] dom E)
(Hlc1: lc t1') (Hfv1: fv t1' [<=] add x1 (dom E))
(Hlc2: lc t2') (Hfv2: fv t2' [<=] add x2 (dom E)),
Interp E t Hlc Hfv =
let R := Interp E t0 Hlc0 Hfv0 in
let R1 := Interp (x1 ¬ RelCompose R (RelSumL RelEqVal RelBot) ++ E) t1' Hlc1 Hfv1 in
let R2 := Interp (x2 ¬ RelCompose R (RelSumL RelBot RelEqVal) ++ E) t2' Hlc2 Hfv2 in
RelUnion
(RelLet (dom E) x1 (RelCompose R (RelSumL RelEqVal RelBot)) R1)
(RelLet (dom E) x2 (RelCompose R (RelSumL RelBot RelEqVal)) R2)
end.
Proof.
apply term_recurse_equations with (Hlc0 := Hlc) (Hfv0 := Hfv).
Qed.
match t with
| BVar _ ⇒ False
| Var x ⇒
∃ Rx, get x E = Some Rx ∧
Interp E t Hlc Hfv = RelInter (RelSelf (Var x)) (RelGather E)
| Let t1 t2 ⇒
∃ x (Hx: x `notin` dom E) t2' (Heq: t2 = close x t2')
(Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E)
(Hlc2: lc t2') (Hfv2: fv t2' [<=] add x (dom E)),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
let R2 := Interp (x ¬ R1 ++ E) t2' Hlc2 Hfv2 in
RelLet (dom E) x R1 R2
| Lam t1 ⇒
∃ x (Hx: x `notin` dom E) t1' (Heq: t1 = close x t1')
(Hlc1: lc t1') (Hfv1: fv t1' [<=] add x (dom E)),
Interp E t Hlc Hfv =
let R := Interp (x ¬ RelTopEnvVal ++ E) t1' Hlc1 Hfv1 in
RelInter (RelLam (dom E) x RelTopEnvVal R)
(RelInter (RelSelf (Lam (close x t1'))) (RelGather E))
| App t1 t2 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
let R2 := Interp E t2 Hlc2 Hfv2 in
APP R1 R2
| Unit ⇒
Interp E t Hlc Hfv = RelInter RelUnitR (RelGather E)
| Pair t1 t2 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
let R2 := Interp E t2 Hlc2 Hfv2 in
RelPairR R1 R2
| Fst t1 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
RelCompose R1 (RelPairL RelEqVal RelTopVal)
| Snd t1 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
RelCompose R1 (RelPairL RelTopVal RelEqVal)
| InjL t1 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
RelSumR R1 RelBot
| InjR t1 ⇒
∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E),
Interp E t Hlc Hfv =
let R1 := Interp E t1 Hlc1 Hfv1 in
RelSumR RelBot R1
| Match t0 t1 t2 ⇒
∃ x1 (Hx1: x1 `notin` dom E) t1' (Heq: t1 = close x1 t1')
x2 (Hx2: x2 `notin` dom E) t2' (Heq: t2 = close x2 t2')
(Hlc0: lc t0) (Hfv0: fv t0 [<=] dom E)
(Hlc1: lc t1') (Hfv1: fv t1' [<=] add x1 (dom E))
(Hlc2: lc t2') (Hfv2: fv t2' [<=] add x2 (dom E)),
Interp E t Hlc Hfv =
let R := Interp E t0 Hlc0 Hfv0 in
let R1 := Interp (x1 ¬ RelCompose R (RelSumL RelEqVal RelBot) ++ E) t1' Hlc1 Hfv1 in
let R2 := Interp (x2 ¬ RelCompose R (RelSumL RelBot RelEqVal) ++ E) t2' Hlc2 Hfv2 in
RelUnion
(RelLet (dom E) x1 (RelCompose R (RelSumL RelEqVal RelBot)) R1)
(RelLet (dom E) x2 (RelCompose R (RelSumL RelBot RelEqVal)) R2)
end.
Proof.
apply term_recurse_equations with (Hlc0 := Hlc) (Hfv0 := Hfv).
Qed.
The above definition does not depend on the proof terms for lc
and for the inclusion of free variables.
Lemma Interp_proof_irrelevant E1 E2 (Henv_eq: E1 = E2) t1 t2 (Heq: t1 = t2)
(Hlc1: lc t1) (Hlc2: lc t2) (Hfv1: fv t1 [<=] dom E1) (Hfv2: fv t2 [<=] dom E2) :
Interp E1 t1 Hlc1 Hfv1 = Interp E2 t2 Hlc2 Hfv2.
Proof.
apply term_recurse_proof_irrelevant; auto.
Qed.
Section Ind.
(Hlc1: lc t1) (Hlc2: lc t2) (Hfv1: fv t1 [<=] dom E1) (Hfv2: fv t2 [<=] dom E2) :
Interp E1 t1 Hlc1 Hfv1 = Interp E2 t2 Hlc2 Hfv2.
Proof.
apply term_recurse_proof_irrelevant; auto.
Qed.
Section Ind.
Arguments of the induction principle.
Context (P: ∀ (E: env (rel (env term) term)) (t: term) (R: rel (env term) term), Prop)
(HVar: ∀ E x (Hx: x `in` dom E)
(Hlc: lc (Var x))
(Hfv: fv (Var x) [<=] dom E)
R (Hget: get x E = Some R),
P E (Var x) (RelInter (RelSelf (Var x)) (RelGather E))
)
(HLet: ∀ E x (Hx: x `notin` dom E),
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x (dom E)) R2
(Heq2: Interp (x ¬ R1 ++ E) t2 Hlc2 Hfv2 = R2)
(IH2: P (x ¬ R1 ++ E) t2 R2),
∀ (Hlc: lc (Let t1 (close x t2)))
(Hfv: fv (Let t1 (close x t2)) [<=] dom E),
P E (Let t1 (close x t2)) (RelLet (dom E) x R1 R2)
)
(HLam: ∀ E x (Hx: x `notin` dom E),
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] add x (dom E)) R1
(Heq1: Interp (x ¬ RelTopEnvVal ++ E) t1 Hlc1 Hfv1 = R1)
(IH1: P (x ¬ RelTopEnvVal ++ E) t1 R1),
∀ (Hlc: lc (Lam (close x t1)))
(Hfv: fv (Lam (close x t1)) [<=] dom E),
P E (Lam (close x t1))
(RelInter (RelLam (dom E) x RelTopEnvVal R1)
(RelInter (RelSelf (Lam (close x t1))) (RelGather E)))
)
(HApp: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E) R2
(Heq2: Interp E t2 Hlc2 Hfv2 = R2)
(IH2: P E t2 R2),
∀ (Hlc: lc (App t1 t2))
(Hfv: fv (App t1 t2) [<=] dom E),
P E (App t1 t2) (APP R1 R2)
)
(HUnit: ∀ E (Hlc: lc Unit) (Hfv: fv Unit [<=] dom E),
P E Unit (RelInter RelUnitR (RelGather E))
)
(HPair: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E) R2
(Heq2: Interp E t2 Hlc2 Hfv2 = R2)
(IH2: P E t2 R2),
∀ (Hlc: lc (Pair t1 t2))
(Hfv: fv (Pair t1 t2) [<=] dom E),
P E (Pair t1 t2) (RelPairR R1 R2)
)
(HFst: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ (Hlc: lc (Fst t1)) (Hfv: fv (Fst t1) [<=] dom E),
P E (Fst t1) (RelCompose R1 (RelPairL RelEqVal RelTopVal))
)
(HSnd: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ (Hlc: lc (Snd t1)) (Hfv: fv (Snd t1) [<=] dom E),
P E (Snd t1) (RelCompose R1 (RelPairL RelTopVal RelEqVal))
)
(HInjL: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ (Hlc: lc (InjL t1)) (Hfv: fv (InjL t1) [<=] dom E),
P E (InjL t1) (RelSumR R1 RelBot)
)
(HInjR: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ (Hlc: lc (InjR t1)) (Hfv: fv (InjR t1) [<=] dom E),
P E (InjR t1) (RelSumR RelBot R1)
)
(HMatch: ∀ E x2 (Hx2: x2 `notin` dom E) x3 (Hx3: x3 `notin` dom E),
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x2 (dom E)) R2
(Heq2: Interp (x2 ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E) t2 Hlc2 Hfv2 = R2)
(IH2: P (x2 ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E) t2 R2),
∀ t3 (Hlc3: lc t3) (Hfv3: fv t3 [<=] add x3 (dom E)) R3
(Heq3: Interp (x3 ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E) t3 Hlc3 Hfv3 = R3)
(IH3: P (x3 ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E) t3 R3),
∀ (Hlc: lc (Match t1 (close x2 t2) (close x3 t3)))
(Hfv: fv (Match t1 (close x2 t2) (close x3 t3)) [<=] dom E),
P E (Match t1 (close x2 t2) (close x3 t3))
(RelUnion
(RelLet (dom E) x2 (RelCompose R1 (RelSumL RelEqVal RelBot)) R2)
(RelLet (dom E) x3 (RelCompose R1 (RelSumL RelBot RelEqVal)) R3))
)
.
(HVar: ∀ E x (Hx: x `in` dom E)
(Hlc: lc (Var x))
(Hfv: fv (Var x) [<=] dom E)
R (Hget: get x E = Some R),
P E (Var x) (RelInter (RelSelf (Var x)) (RelGather E))
)
(HLet: ∀ E x (Hx: x `notin` dom E),
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x (dom E)) R2
(Heq2: Interp (x ¬ R1 ++ E) t2 Hlc2 Hfv2 = R2)
(IH2: P (x ¬ R1 ++ E) t2 R2),
∀ (Hlc: lc (Let t1 (close x t2)))
(Hfv: fv (Let t1 (close x t2)) [<=] dom E),
P E (Let t1 (close x t2)) (RelLet (dom E) x R1 R2)
)
(HLam: ∀ E x (Hx: x `notin` dom E),
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] add x (dom E)) R1
(Heq1: Interp (x ¬ RelTopEnvVal ++ E) t1 Hlc1 Hfv1 = R1)
(IH1: P (x ¬ RelTopEnvVal ++ E) t1 R1),
∀ (Hlc: lc (Lam (close x t1)))
(Hfv: fv (Lam (close x t1)) [<=] dom E),
P E (Lam (close x t1))
(RelInter (RelLam (dom E) x RelTopEnvVal R1)
(RelInter (RelSelf (Lam (close x t1))) (RelGather E)))
)
(HApp: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E) R2
(Heq2: Interp E t2 Hlc2 Hfv2 = R2)
(IH2: P E t2 R2),
∀ (Hlc: lc (App t1 t2))
(Hfv: fv (App t1 t2) [<=] dom E),
P E (App t1 t2) (APP R1 R2)
)
(HUnit: ∀ E (Hlc: lc Unit) (Hfv: fv Unit [<=] dom E),
P E Unit (RelInter RelUnitR (RelGather E))
)
(HPair: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E) R2
(Heq2: Interp E t2 Hlc2 Hfv2 = R2)
(IH2: P E t2 R2),
∀ (Hlc: lc (Pair t1 t2))
(Hfv: fv (Pair t1 t2) [<=] dom E),
P E (Pair t1 t2) (RelPairR R1 R2)
)
(HFst: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ (Hlc: lc (Fst t1)) (Hfv: fv (Fst t1) [<=] dom E),
P E (Fst t1) (RelCompose R1 (RelPairL RelEqVal RelTopVal))
)
(HSnd: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ (Hlc: lc (Snd t1)) (Hfv: fv (Snd t1) [<=] dom E),
P E (Snd t1) (RelCompose R1 (RelPairL RelTopVal RelEqVal))
)
(HInjL: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ (Hlc: lc (InjL t1)) (Hfv: fv (InjL t1) [<=] dom E),
P E (InjL t1) (RelSumR R1 RelBot)
)
(HInjR: ∀ E,
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ (Hlc: lc (InjR t1)) (Hfv: fv (InjR t1) [<=] dom E),
P E (InjR t1) (RelSumR RelBot R1)
)
(HMatch: ∀ E x2 (Hx2: x2 `notin` dom E) x3 (Hx3: x3 `notin` dom E),
∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
(Heq1: Interp E t1 Hlc1 Hfv1 = R1)
(IH1: P E t1 R1),
∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x2 (dom E)) R2
(Heq2: Interp (x2 ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E) t2 Hlc2 Hfv2 = R2)
(IH2: P (x2 ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E) t2 R2),
∀ t3 (Hlc3: lc t3) (Hfv3: fv t3 [<=] add x3 (dom E)) R3
(Heq3: Interp (x3 ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E) t3 Hlc3 Hfv3 = R3)
(IH3: P (x3 ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E) t3 R3),
∀ (Hlc: lc (Match t1 (close x2 t2) (close x3 t3)))
(Hfv: fv (Match t1 (close x2 t2) (close x3 t3)) [<=] dom E),
P E (Match t1 (close x2 t2) (close x3 t3))
(RelUnion
(RelLet (dom E) x2 (RelCompose R1 (RelSumL RelEqVal RelBot)) R2)
(RelLet (dom E) x3 (RelCompose R1 (RelSumL RelBot RelEqVal)) R3))
)
.
Induction principle.
Lemma Interp_ind E t (Hlc: lc t) (Hfv: fv t [<=] dom E) :
P E t (Interp E t Hlc Hfv).
Proof.
unfold Interp.
apply term_induction; auto.
Qed.
End Ind.
P E t (Interp E t Hlc Hfv).
Proof.
unfold Interp.
apply term_induction; auto.
Qed.
End Ind.
Assuming the environment is well supported, Interp produces a
relation that is supported by the domain of the environment.
Lemma Interp_supported E t (Hlc: lc t) (Hfv: fv t [<=] dom E):
well_supported_env E →
supported_rel (dom E) (Interp E t Hlc Hfv).
Proof.
apply Interp_ind; clear E t Hlc Hfv; intros; auto with supported_rel.
- apply RelInter_supported_rel.
+ apply (supported_rel_subset (fv (Var x))); eauto.
apply RelSelf_supported_rel.
+ apply RelGather_supported_rel. auto.
- apply RelLet_supported; auto; try reflexivity.
apply IH2.
simpl. split; auto.
- apply RelInter_supported_rel; [| apply RelInter_supported_rel ].
+ apply RelLam_supported; auto with good_rel supported_rel.
apply IH1.
simpl. split; auto with supported_rel.
+ apply (supported_rel_subset (fv (Lam (close x t1)))); auto.
apply RelSelf_supported_rel.
+ apply RelGather_supported_rel. auto.
- assert (supported_rel (dom E) R1) by auto.
apply RelUnion_supported_rel.
+ apply RelLet_supported; auto with supported_rel.
apply IH2. simpl.
split; auto with supported_rel.
+ apply RelLet_supported; auto with supported_rel.
apply IH3. simpl.
split; auto with supported_rel.
Qed.
Hint Resolve Interp_supported: supported_rel.
well_supported_env E →
supported_rel (dom E) (Interp E t Hlc Hfv).
Proof.
apply Interp_ind; clear E t Hlc Hfv; intros; auto with supported_rel.
- apply RelInter_supported_rel.
+ apply (supported_rel_subset (fv (Var x))); eauto.
apply RelSelf_supported_rel.
+ apply RelGather_supported_rel. auto.
- apply RelLet_supported; auto; try reflexivity.
apply IH2.
simpl. split; auto.
- apply RelInter_supported_rel; [| apply RelInter_supported_rel ].
+ apply RelLam_supported; auto with good_rel supported_rel.
apply IH1.
simpl. split; auto with supported_rel.
+ apply (supported_rel_subset (fv (Lam (close x t1)))); auto.
apply RelSelf_supported_rel.
+ apply RelGather_supported_rel. auto.
- assert (supported_rel (dom E) R1) by auto.
apply RelUnion_supported_rel.
+ apply RelLet_supported; auto with supported_rel.
apply IH2. simpl.
split; auto with supported_rel.
+ apply RelLet_supported; auto with supported_rel.
apply IH3. simpl.
split; auto with supported_rel.
Qed.
Hint Resolve Interp_supported: supported_rel.
Assuming the environment is wellformed, Interp produces a
relation that is wellformed for the domain of the environment.
Lemma Interp_wf E t (Hlc: lc t) (Hfv: fv t [<=] dom E):
wf_env_rel E →
wf_rel (dom E) (Interp E t Hlc Hfv).
Proof.
apply Interp_ind; intros; auto with wf_rel.
- apply wf_rel_RelInter.
+ apply wf_rel_RelSelf. simpl. fsetdec.
+ apply wf_rel_RelGather; auto. reflexivity.
- apply wf_rel_RelInter; [| apply wf_rel_RelInter]; auto with wf_rel.
apply wf_rel_RelGather; auto. reflexivity.
- apply wf_rel_RelInter; auto with wf_rel.
apply wf_rel_RelGather; auto. reflexivity.
- apply wf_rel_RelUnion; apply wf_rel_RelLet; auto with wf_rel.
Qed.
Hint Resolve Interp_wf : wf_rel.
wf_env_rel E →
wf_rel (dom E) (Interp E t Hlc Hfv).
Proof.
apply Interp_ind; intros; auto with wf_rel.
- apply wf_rel_RelInter.
+ apply wf_rel_RelSelf. simpl. fsetdec.
+ apply wf_rel_RelGather; auto. reflexivity.
- apply wf_rel_RelInter; [| apply wf_rel_RelInter]; auto with wf_rel.
apply wf_rel_RelGather; auto. reflexivity.
- apply wf_rel_RelInter; auto with wf_rel.
apply wf_rel_RelGather; auto. reflexivity.
- apply wf_rel_RelUnion; apply wf_rel_RelLet; auto with wf_rel.
Qed.
Hint Resolve Interp_wf : wf_rel.
Soundness lemma for Interp
Lemma Interp_soundness E t (Hlc: lc t) (Hfv: fv t [<=] dom E):
wf_env_rel E →
RelIncl (Rsem E t) (Interp E t Hlc Hfv).
Proof.
apply Interp_ind; clear E t Hlc Hfv; intros.
- apply Rsem_RelIncl_Var; auto.
- rewrite <- IH1; auto.
rewrite <- IH2; auto.
+ assert (env_rel_incl (x ¬ (Rsem E t1) ++ E) (x ¬ R1 ++ E)) as Hincl.
{ simpl. split; [| split]; auto. reflexivity. }
rewrite <- Hincl.
apply Rsem_RelIncl_Let; auto with wf_rel.
+ apply wf_env_rel_cons; subst; eauto using Interp_wf.
- rewrite <- IH1; auto with wf_rel.
apply Rsem_RelIncl_RelLam; auto with wf_rel.
- rewrite <- IH1; auto.
rewrite <- IH2; auto.
apply Rsem_RelIncl_App.
- apply Rsem_RelIncl_Unit; auto.
- rewrite <- IH1; auto.
rewrite <- IH2; auto.
apply Rsem_RelIncl_Pair.
- rewrite <- IH1; auto.
apply Rsem_RelIncl_Fst; auto.
- rewrite <- IH1; auto.
apply Rsem_RelIncl_Snd; auto.
- rewrite <- IH1; auto.
apply Rsem_RelIncl_InjL.
- rewrite <- IH1; auto.
apply Rsem_RelIncl_InjR.
- assert (wf_rel (dom E) R1) by (subst R1; auto with wf_rel).
rewrite <- IH1; auto.
rewrite <- IH2; auto with wf_rel.
rewrite <- IH3; auto with wf_rel.
assert (env_rel_incl (x2 ¬ (RelCompose (Rsem E t1) (RelSumL RelEqVal RelBot)) ++ E)
(x2 ¬ (RelCompose R1 (RelSumL RelEqVal RelBot)) ++ E))
as Hincl2.
{ simpl. split; [| split]; auto.
- rewrite IH1; auto. reflexivity.
- reflexivity.
}
rewrite <- Hincl2. clear Hincl2.
assert (env_rel_incl (x3 ¬ (RelCompose (Rsem E t1) (RelSumL RelBot RelEqVal)) ++ E)
(x3 ¬ (RelCompose R1 (RelSumL RelBot RelEqVal)) ++ E))
as Hincl3.
{ simpl. split; [| split]; auto.
- rewrite IH1; auto. reflexivity.
- reflexivity.
}
rewrite <- Hincl3. clear Hincl3.
apply Rsem_RelIncl_Match; auto.
Qed.
wf_env_rel E →
RelIncl (Rsem E t) (Interp E t Hlc Hfv).
Proof.
apply Interp_ind; clear E t Hlc Hfv; intros.
- apply Rsem_RelIncl_Var; auto.
- rewrite <- IH1; auto.
rewrite <- IH2; auto.
+ assert (env_rel_incl (x ¬ (Rsem E t1) ++ E) (x ¬ R1 ++ E)) as Hincl.
{ simpl. split; [| split]; auto. reflexivity. }
rewrite <- Hincl.
apply Rsem_RelIncl_Let; auto with wf_rel.
+ apply wf_env_rel_cons; subst; eauto using Interp_wf.
- rewrite <- IH1; auto with wf_rel.
apply Rsem_RelIncl_RelLam; auto with wf_rel.
- rewrite <- IH1; auto.
rewrite <- IH2; auto.
apply Rsem_RelIncl_App.
- apply Rsem_RelIncl_Unit; auto.
- rewrite <- IH1; auto.
rewrite <- IH2; auto.
apply Rsem_RelIncl_Pair.
- rewrite <- IH1; auto.
apply Rsem_RelIncl_Fst; auto.
- rewrite <- IH1; auto.
apply Rsem_RelIncl_Snd; auto.
- rewrite <- IH1; auto.
apply Rsem_RelIncl_InjL.
- rewrite <- IH1; auto.
apply Rsem_RelIncl_InjR.
- assert (wf_rel (dom E) R1) by (subst R1; auto with wf_rel).
rewrite <- IH1; auto.
rewrite <- IH2; auto with wf_rel.
rewrite <- IH3; auto with wf_rel.
assert (env_rel_incl (x2 ¬ (RelCompose (Rsem E t1) (RelSumL RelEqVal RelBot)) ++ E)
(x2 ¬ (RelCompose R1 (RelSumL RelEqVal RelBot)) ++ E))
as Hincl2.
{ simpl. split; [| split]; auto.
- rewrite IH1; auto. reflexivity.
- reflexivity.
}
rewrite <- Hincl2. clear Hincl2.
assert (env_rel_incl (x3 ¬ (RelCompose (Rsem E t1) (RelSumL RelBot RelEqVal)) ++ E)
(x3 ¬ (RelCompose R1 (RelSumL RelBot RelEqVal)) ++ E))
as Hincl3.
{ simpl. split; [| split]; auto.
- rewrite IH1; auto. reflexivity.
- reflexivity.
}
rewrite <- Hincl3. clear Hincl3.
apply Rsem_RelIncl_Match; auto.
Qed.
Completeness for Interp
Lemma Interp_completeness E t (Hlc: lc t) (Hfv: fv t [<=] dom E):
uniq E →
wf_env_rel E →
RelIncl (Interp E t Hlc Hfv) (Rsem E t).
Proof.
apply Interp_ind; clear E t Hlc Hfv; intros.
- apply RelIncl_Rsem_Self_Gather; auto.
- rewrite IH1; auto.
assert (wf_env_rel (x ¬ R1 ++ E)) as Hwfenv1.
{ subst R1. auto with wf_rel. }
rewrite IH2; auto.
assert (env_rel_incl (x ¬ R1 ++ E) (x ¬ (Rsem E t1) ++ E)) as Hincl.
{ simpl. split; [| split]; auto. reflexivity. }
rewrite Hincl. clear Hincl.
apply RelIncl_Rsem_Let; auto.
- rewrite RelInter_lb2.
apply RelIncl_Rsem_Self_Gather; auto.
- rewrite IH1; auto.
rewrite IH2; auto.
apply RelIncl_Rsem_App; auto.
- apply RelIncl_Rsem_Unit; auto.
- rewrite IH1; auto.
rewrite IH2; auto.
apply RelIncl_Rsem_Pair; auto.
- rewrite IH1; auto.
apply RelIncl_Rsem_Fst; auto.
- rewrite IH1; auto.
apply RelIncl_Rsem_Snd; auto.
- rewrite IH1; auto.
apply RelIncl_Rsem_InjL; auto.
- rewrite IH1; auto.
apply RelIncl_Rsem_InjR; auto.
- assert (wf_rel (dom E) R1) by (subst R1; auto with wf_rel).
rewrite IH1; auto.
rewrite IH2; auto with wf_rel.
rewrite IH3; auto with wf_rel.
assert (env_rel_incl (x2 ¬ (RelCompose R1 (RelSumL RelEqVal RelBot)) ++ E)
(x2 ¬ (RelCompose (Rsem E t1) (RelSumL RelEqVal RelBot)) ++ E))
as Hincl2.
{ simpl. split; [| split]; auto.
- rewrite IH1; auto. reflexivity.
- reflexivity.
}
rewrite Hincl2. clear Hincl2.
assert (env_rel_incl (x3 ¬ (RelCompose R1 (RelSumL RelBot RelEqVal)) ++ E)
(x3 ¬ (RelCompose (Rsem E t1) (RelSumL RelBot RelEqVal)) ++ E))
as Hincl3.
{ simpl. split; [| split]; auto.
- rewrite IH1; auto. reflexivity.
- reflexivity.
}
rewrite Hincl3. clear Hincl3.
apply RelIncl_Rsem_Match; auto.
Qed.
uniq E →
wf_env_rel E →
RelIncl (Interp E t Hlc Hfv) (Rsem E t).
Proof.
apply Interp_ind; clear E t Hlc Hfv; intros.
- apply RelIncl_Rsem_Self_Gather; auto.
- rewrite IH1; auto.
assert (wf_env_rel (x ¬ R1 ++ E)) as Hwfenv1.
{ subst R1. auto with wf_rel. }
rewrite IH2; auto.
assert (env_rel_incl (x ¬ R1 ++ E) (x ¬ (Rsem E t1) ++ E)) as Hincl.
{ simpl. split; [| split]; auto. reflexivity. }
rewrite Hincl. clear Hincl.
apply RelIncl_Rsem_Let; auto.
- rewrite RelInter_lb2.
apply RelIncl_Rsem_Self_Gather; auto.
- rewrite IH1; auto.
rewrite IH2; auto.
apply RelIncl_Rsem_App; auto.
- apply RelIncl_Rsem_Unit; auto.
- rewrite IH1; auto.
rewrite IH2; auto.
apply RelIncl_Rsem_Pair; auto.
- rewrite IH1; auto.
apply RelIncl_Rsem_Fst; auto.
- rewrite IH1; auto.
apply RelIncl_Rsem_Snd; auto.
- rewrite IH1; auto.
apply RelIncl_Rsem_InjL; auto.
- rewrite IH1; auto.
apply RelIncl_Rsem_InjR; auto.
- assert (wf_rel (dom E) R1) by (subst R1; auto with wf_rel).
rewrite IH1; auto.
rewrite IH2; auto with wf_rel.
rewrite IH3; auto with wf_rel.
assert (env_rel_incl (x2 ¬ (RelCompose R1 (RelSumL RelEqVal RelBot)) ++ E)
(x2 ¬ (RelCompose (Rsem E t1) (RelSumL RelEqVal RelBot)) ++ E))
as Hincl2.
{ simpl. split; [| split]; auto.
- rewrite IH1; auto. reflexivity.
- reflexivity.
}
rewrite Hincl2. clear Hincl2.
assert (env_rel_incl (x3 ¬ (RelCompose R1 (RelSumL RelBot RelEqVal)) ++ E)
(x3 ¬ (RelCompose (Rsem E t1) (RelSumL RelBot RelEqVal)) ++ E))
as Hincl3.
{ simpl. split; [| split]; auto.
- rewrite IH1; auto. reflexivity.
- reflexivity.
}
rewrite Hincl3. clear Hincl3.
apply RelIncl_Rsem_Match; auto.
Qed.
Adequacy. This is Theorem 4.7 of the ICFP'20 paper.
Theorem Interp_adequacy E t (Hlc: lc t) (Hfv: fv t [<=] dom E):
uniq E →
wf_env_rel E →
RelEquiv (Interp E t Hlc Hfv) (Rsem E t).
Proof.
intros Huniq Hwf H.
apply RelIncl_antisym; eauto using Interp_soundness, Interp_completeness.
Qed.
Lemma fv_steps_below S t1 t2:
steps t1 t2 →
fv t1 [<=] S →
fv t2 [<=] S.
Proof.
intros Hsteps H.
rewrite <- H. apply steps_fv. assumption.
Qed.
Lemma eval_steps_below S t v:
eval t v →
fv t [<=] S →
fv v [<=] S.
Proof.
intros Heval H.
rewrite <- H. apply eval_fv. assumption.
Qed.
uniq E →
wf_env_rel E →
RelEquiv (Interp E t Hlc Hfv) (Rsem E t).
Proof.
intros Huniq Hwf H.
apply RelIncl_antisym; eauto using Interp_soundness, Interp_completeness.
Qed.
Lemma fv_steps_below S t1 t2:
steps t1 t2 →
fv t1 [<=] S →
fv t2 [<=] S.
Proof.
intros Hsteps H.
rewrite <- H. apply steps_fv. assumption.
Qed.
Lemma eval_steps_below S t v:
eval t v →
fv t [<=] S →
fv v [<=] S.
Proof.
intros Heval H.
rewrite <- H. apply eval_fv. assumption.
Qed.
Lemma Interp_preservation_steps E t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) t2:
uniq E →
wf_env_rel E →
∀ (Hsteps: steps t1 t2),
RelIncl
(Interp E t2 (steps_lc _ _ Hsteps Hlc1) (fv_steps_below _ _ _ Hsteps Hfv1))
(Interp E t1 Hlc1 Hfv1).
Proof.
intros Huniq Hwf Hsteps.
rewrite Interp_adequacy; auto.
rewrite Interp_adequacy; auto.
apply Collecting_steps.
assumption.
Qed.
uniq E →
wf_env_rel E →
∀ (Hsteps: steps t1 t2),
RelIncl
(Interp E t2 (steps_lc _ _ Hsteps Hlc1) (fv_steps_below _ _ _ Hsteps Hfv1))
(Interp E t1 Hlc1 Hfv1).
Proof.
intros Huniq Hwf Hsteps.
rewrite Interp_adequacy; auto.
rewrite Interp_adequacy; auto.
apply Collecting_steps.
assumption.
Qed.
Preservation: eval makes Interp decrease.
Lemma Interp_preservation_eval E t (Hlc: lc t) (Hfv: fv t [<=] dom E) v:
uniq E →
wf_env_rel E →
∀ (Heval: eval t v),
RelIncl
(Interp E v (eval_lc _ _ Heval Hlc) (eval_steps_below _ _ _ Heval Hfv))
(Interp E t Hlc Hfv).
Proof.
intros Huniq Hwf [Hsteps Hvalue].
erewrite (Interp_proof_irrelevant E _ eq_refl v _ eq_refl).
eapply Interp_preservation_steps; eauto.
Unshelve.
- assumption.
Qed.
uniq E →
wf_env_rel E →
∀ (Heval: eval t v),
RelIncl
(Interp E v (eval_lc _ _ Heval Hlc) (eval_steps_below _ _ _ Heval Hfv))
(Interp E t Hlc Hfv).
Proof.
intros Huniq Hwf [Hsteps Hvalue].
erewrite (Interp_proof_irrelevant E _ eq_refl v _ eq_refl).
eapply Interp_preservation_steps; eauto.
Unshelve.
- assumption.
Qed.