@ -47,33 +47,94 @@ Section existential.
TY n ; < [ x := A ] > ( < [ f := ( A → B ) % ty ] > Γ ) ⊢ e : B →
TY n ; Γ ⊢ ( fix : f x := e ) : ( A → B ) ) .
Definition ISET : type := # 0 . (* TODO: your definition *)
Definition ISET : type := ( ∃ :
# 0 × ( Int → # 0 )
× ( # 0 → # 0 → # 0 )
× ( # 0 → # 0 → Bool )
) .
(* We represent sets as functions of type ( ( Int → Bool ) × × ) ,
storing the mapping , the minimum value , and the maximum value . * )
Definition iset : val := # 0 . (* TODO: your definition *)
(*
Let α = ( Int → Bool ) × Int × Int = {
is_mem : Int -> Bool ,
min : Int ,
max : Int
} st . ∀ s : α ,
• ∀ x < s . min , s . is_mem x ~ > * false
• ∀ x > s . max , s . is_mem x ~ > * false
As such , the empty set is ` ( ( λ _ . false ) , 0 , 0 ) `
ISET = sig
type α - - ommitted , part of ∃
empty : α
singleton : Int -> α
union : α -> α -> α
subset : α -> α -> bool
end
* )
Definition subset_helper : expr := ( λ : " a " " b " , ( fix : " rec " " x " := (
if : ( ( Snd " a " ) < " x " ) then
( Lit true )
else
(
if : ( ( Fst ( Fst " a " ) ) " x " ) then
(
if : ( ( Fst ( Fst " b " ) ) " x " ) then
( " rec " ( " x " + ( Lit 1 ) ) )
else
( Lit false )
)
else
" rec " ( " x " + ( Lit 1 ) )
)
) ) ) .
Definition iset : val := ( pack (
( ( λ : BAnon , ( Lit false ) ) , ( LitV 0 ) , ( LitV 0 ) ) ,
( λ : " x " , ( ( λ : " y " , " x " = " y " ) , " x " , " x " ) ) ,
( λ : " a " " b " , (
( λ : " y " , if : ( ( Fst ( Fst " a " ) ) ) " y " then ( ( Fst ( Fst " b " ) ) " y " ) else ( Lit false ) ) ,
if : ( Snd ( Fst " a " ) ) < ( Snd ( Fst " b " ) ) then ( Snd ( Fst " a " ) ) else ( Snd ( Fst " b " ) ) ,
if : ( Snd " b " ) < ( Snd " a " ) then ( Snd " a " ) else ( Snd " b " )
) ) ,
( λ : " a " " b " , (
subset_helper " a " " b " ( Snd ( Fst " a " ) )
) )
) ) .
Lemma iset_typed n Γ : TY n ; Γ ⊢ iset : ISET .
Proof .
(* HINT: use repeated solve_typing with an explicit apply fix_typing inbetween *)
(* TODO: exercise *)
Admitted .
Definition ISETE : type := # 0 . (* TODO: your definition *)
Definition add_equality : val := # 0 . (* TODO: your definition *)
repeat solve_typing .
eapply fix_typing ; try eauto .
repeat solve_typing .
Qed .
Definition ISETE : type := ( ∃ :
# 0 × ( Int → # 0 )
× ( # 0 → # 0 → # 0 )
× ( # 0 → # 0 → Bool )
× ( # 0 → # 0 → Bool )
) .
Definition add_equality : val := ( λ : " impl " , unpack " impl " as " impl2 " in ( pack (
( Fst ( Fst " impl2 " ) ) ,
( Snd ( Fst " impl2 " ) ) ,
( Snd " impl2 " ) ,
( λ : " a " " b " , if : ( ( Snd " impl2 " ) " a " " b " ) then
( ( Snd " impl2 " ) " b " " a " )
else
( Lit false )
)
) ) ) .
Lemma add_equality_typed n Γ : TY n ; Γ ⊢ add_equality : ( ISET → ISETE ) % ty .
Proof .
repeat solve_typing .
(* Qed. *)
(* TODO: exercise *)
Admitted .
Qed .
End existential .
Section ex4 .
@ -101,23 +162,109 @@ Context (even_dec_typed : ∀ n Γ, TY n; Γ ⊢ even_dec : (Int → Bool)).
You may use the [ assert ] expression defined in existential_invariants . v .
* )
Definition even_impl_instrumented : val := # 0 . (* TODO: your definition *)
Definition even_impl_instrumented : val := pack ( # 0 ,
λ : " z " , # 2 + " z " ,
λ : " z " , ( Snd ( assert ( even_dec " z " ) , " z " ) )
) . (* TODO: your definition *)
(* b ) Prove that [even_impl_instrumented] is safe. You may assume that even works as intended,
but be sure to state this here . * )
Context ( even_dec_correct : ∀ n , big_step ( even_dec ( Lit ( 2 * n ) % Z ) ) # true ) .
Lemma even_impl_instrumented_safe δ :
𝒱 even_type δ even_impl_instrumented .
Proof .
(* TODO: exercise *)
Admitted .
unfold even_type .
simp type_interp .
eexists ; split ; first reflexivity .
(* Pick τ such that it only contains even integers *)
pose_sem_type ( fun n => match n with
| LitV ( LitInt n' ) => ∃ ( x : Z ) , ( 2 * x ) % Z = n'
| _ => False
end
) as τ .
{
intros v h_v .
destruct v ; try ( exfalso ; exact h_v ) .
destruct l ; try ( exfalso ; exact h_v ) .
auto .
}
exists τ .
simp type_interp .
eexists ; eexists ; split ; last split ; first reflexivity .
- simp type_interp .
(* Quickly prove that 0 ∈ V[τ] *)
eexists ; eexists ; split ; first reflexivity .
split .
simp type_interp ; simpl .
exists 0 ; eauto .
(* Prove that ( λ: "z", 2 + "z" ) ∈ V[τ → τ] *)
simp type_interp .
eexists ; eexists ; split ; last split ; first reflexivity .
eauto .
(* Intro a value z *)
intros z z_tau .
(* Invert z using z_tau *)
simp type_interp in z_tau ; simpl in z_tau .
destruct z ; try ( exfalso ; exact z_tau ) .
destruct l ; try ( exfalso ; exact z_tau ) .
simp type_interp ; exists ( LitV ( 2 + n ) % Z ) ; simpl ; split .
econstructor ; try econstructor .
(* Prove that 2+n ∈ V[τ] *)
simp type_interp ; simpl .
destruct z_tau as [ x z_tau ] .
exists ( x + 1 ) % Z .
rewrite <- z_tau .
lia .
- simp type_interp .
(* Small detour to prove closedness *)
have even_dec_closed : is_closed [] even_dec .
{
apply ( syn_typed_closed 0 ∅ _ _ _ ( even_dec_typed 0 ∅ ) ) .
intros x falsity ; exfalso .
rewrite dom_empty in falsity .
rewrite elem_of_empty in falsity .
exact falsity .
}
eexists ; eexists ; split ; last split ; first reflexivity .
{
unfold is_closed ; simpl ; fold is_closed .
repeat rewrite andb_True ; repeat split ; eauto .
apply is_closed_weaken_nil .
assumption .
}
intros z z_tau .
(* We know that z = 2 * z' *)
simp type_interp in * .
simpl in z_tau .
destruct z ; try ( exfalso ; exact z_tau ) .
destruct l ; try ( exfalso ; exact z_tau ) .
exists ( LitV ( LitInt n ) ) .
split .
(* z ∈ V[τ], from our hypothesis *)
2 : simp type_interp ; eexists ; reflexivity .
simpl .
rewrite ( subst_is_closed_nil _ _ _ even_dec_closed ) .
bs_step_det .
(* Finally, we need to prove that `if ( even_dec n ) then ( ) else kaboom` steps to the correct value. *)
econstructor .
destruct z_tau as [ x z_tau ] .
rewrite <- z_tau .
(* We assume that `big_step ( even_dec x ) true` if `x = 2 * x'` *)
exact ( even_dec_correct x ) .
econstructor .
Qed .
End ex4 .
(* * * * Exercise 5 ( LN Exercise 31 ) : Abstract sums *)
Section ex5 .
Import logrel existential_invariants .
Definition sum_ex_type ( A B : type ) : type :=
∃ : ( ( A . [ ren ( + 1 ) ] → # 0 ) ×
( B . [ ren ( + 1 ) ] → # 0 ) ×
@ -130,11 +277,202 @@ Definition sum_ex_impl : val :=
Λ , λ : " x " " f1 " " f2 " , if : Fst " x " = # 1 then " f1 " ( Snd " x " ) else " f2 " ( Snd " x " )
) .
Ltac ℰ _ to_ 𝒱 := simp type_interp ; eexists ; split ; first ( simpl ; econstructor ) .
Ltac 𝒱 _ λ := simp type_interp ; eexists ; eexists ; split ; first reflexivity ; split ; first eauto .
Lemma ren_2 A : A . [ ren ( + 2 ) ] = A . [ ren ( + 1 ) ] . [ ren ( + 1 ) ] .
Proof .
(* Autosubst is not part of the curriculum, so I don't see why I should have to prove this. *)
admit .
Admitted .
Lemma sum_ex_safe A B δ :
𝒱 ( sum_ex_type A B ) δ sum_ex_impl .
Proof .
(* TODO: exercise *)
Admitted .
unfold sum_ex_type .
simp type_interp .
eexists ; split ; first reflexivity .
(*
To prove that ` sum_ex_impl ∈ 𝒱 [ ∃ α , .. . ] ` , we pick a subset τ of SemType such that it models
the invariants of our representation . Namely , let ` τ = { 1 } × 𝒱 [ A ] ∪ { 2 } × 𝒱 [ B ] ` .
* )
remember ( λ v ,
match v with
| PairV ( LitV ( LitInt 1 ) ) w => 𝒱 A δ w
| PairV ( LitV ( LitInt 2 ) ) w => 𝒱 B δ w
| _ => False
end
) as τ _ λ .
have inv_ τ : ∀ v , τ _ λ v → ∃ v' ,
v = ( PairV ( LitV ( LitInt 1 ) ) v' ) ∧ 𝒱 A δ v'
∨ v = ( PairV ( LitV ( LitInt 2 ) ) v' ) ∧ 𝒱 B δ v' .
{
intros v v_in_ τ .
(* There is currently no way to automate this away, thanks to Coq's advantage of being 30-years old *)
rewrite Heq τ _ λ in v_in_ τ .
destruct v ; try ( exfalso ; exact v_in_ τ ) .
destruct v1 ; try ( exfalso ; exact v_in_ τ ) .
destruct l ; try ( exfalso ; exact v_in_ τ ) .
destruct n ; try ( exfalso ; exact v_in_ τ ) .
destruct p ; try ( exfalso ; exact v_in_ τ ) .
destruct p ; try ( exfalso ; exact v_in_ τ ) .
- exists v2 ; right .
split ; [ reflexivity | assumption ] .
- exists v2 ; left .
split ; [ reflexivity | assumption ] .
}
pose_sem_type τ _ λ as τ .
{
intros v v_in_ τ .
destruct ( inv_ τ v v_in_ τ ) as [ v2 [ ( -> & v2_log ) | ( -> & v2_log ) ] ] .
all : simpl .
all : eapply val_rel_closed ; exact v2_log .
}
exists τ .
(* Split the triple into its constitutants *)
simp type_interp ; eexists ; eexists ; split ; first reflexivity ; split .
simp type_interp ; eexists ; eexists ; split ; first reflexivity ; split .
- (* Prove that λx. ( 1, x ) ∈ 𝒱 *)
𝒱 _ λ .
(* Closedness detour *)
eauto .
intros v v_in_A .
simp type_interp ; eexists ; split .
simpl .
(* We know that ( 1, v ) steps to ( 1, v ) *)
econstructor ; ( econstructor | | apply big_step_of_val ; reflexivity ) .
simp type_interp ; simpl .
(* From our choice of τ_λ, ( 1, v ) ∈ τ <-> v ∈ 𝒱 *)
rewrite Heq τ _ λ .
rewrite sem_val_rel_cons .
exact v_in_A .
- (* Prove that λx. ( 2, x ) ∈ 𝒱 *)
𝒱 _ λ .
eauto .
intros v v_in_B .
simp type_interp ; eexists ; split .
simpl .
(* We know that ( 2, v ) steps to ( 2, v ) *)
econstructor ; ( econstructor | | apply big_step_of_val ; reflexivity ) .
simp type_interp ; simpl .
rewrite Heq τ _ λ .
rewrite sem_val_rel_cons .
exact v_in_B .
- (* Prove that our match is in `∀α, τ → ( A → α ) → ( B → β ) → β` *)
simp type_interp .
eexists ; split ; first reflexivity ; split .
eauto .
intro τ ₂ .
(* Given an arbitrary τ₂, show that match ∈ 𝒱 ( A → τ₂ ) → ( B → τ₂ ) → τ] *)
ℰ _ to_ 𝒱 .
𝒱 _ λ .
(* We thus have to prove that for v ∈ τ, the rest works *)
intros v v_in_ τ .
simp type_interp in v_in_ τ ; simpl in v_in_ τ .
simpl .
ℰ _ to_ 𝒱 .
𝒱 _ λ .
{
(* Closedness detour *)
have h_cl : is_closed [] ( of_val v ) .
destruct ( inv_ τ v v_in_ τ ) as [ v2 [ ( -> & v2_log ) | ( -> & v2_log ) ] ] .
all : eauto .
simplify_closed .
}
intros v ₁ v ₁ _ in_Afn .
ℰ _ to_ 𝒱 .
𝒱 _ λ .
{
(* Closedness detour, the detouring *)
have h_cl : is_closed [] ( of_val v ) .
destruct ( inv_ τ v v_in_ τ ) as [ v2 [ ( -> & v2_log ) | ( -> & v2_log ) ] ] .
all : eauto .
simplify_closed .
apply is_closed_weaken_nil .
eapply val_rel_closed .
exact v ₁ _ in_Afn .
}
intros v ₂ v ₂ _ in_Bfn .
have v ₁ _ cl : is_closed [] v ₁ .
{
eapply val_rel_closed .
exact v ₁ _ in_Afn .
}
have v ₂ _ cl : is_closed [] v ₂ .
{
eapply val_rel_closed .
exact v ₂ _ in_Bfn .
}
(* Remove all the noisy substs *)
simpl .
repeat rewrite ( lang . subst_is_closed [] ) ; eauto .
all : try set_solver .
(* By cases on the values that v can take *)
destruct ( inv_ τ v v_in_ τ ) as [ v' [ ( -> & v'_log ) | ( -> & v'_log ) ] ] .
+ (* If v = ( 1, v' ) *)
have v'_in_A' : 𝒱 A . [ ren ( + 2 ) ] ( τ ₂ . : τ . : δ ) v' .
{
rewrite ren_2 .
rewrite <- sem_val_rel_cons .
rewrite <- sem_val_rel_cons .
exact v'_log .
}
(* We can deduce from v₁ ∈ 𝒱 ( v' ) in τ, it will step to a value in τ₂ *)
simp type_interp in v ₁ _ in_Afn .
destruct v ₁ _ in_Afn as ( x ₁ & e' & -> & e ₁ _ cl & v ₁ _ ty ) .
specialize ( v ₁ _ ty v' v'_in_A' ) .
simp type_interp in v ₁ _ ty .
destruct v ₁ _ ty as [ v ₁ ' [ v ₁ _ bs v ₁ ' _ ty ] ] .
simp type_interp .
eexists ; split .
(* We can see that our if-expression steps to ( v₁ v' ) *)
bs_step_det .
eapply bs_if_true .
bs_step_det .
econstructor .
apply big_step_of_val ; reflexivity .
bs_step_det .
(* So we can use the information from v₁ ∈ 𝒱 *)
exact v ₁ _ bs .
exact v ₁ ' _ ty .
+ (* If v = ( 2, v' ) , we do the same thing, but with B *)
have v'_in_B' : 𝒱 B . [ ren ( + 2 ) ] ( τ ₂ . : τ . : δ ) v' .
{
rewrite ren_2 .
rewrite <- sem_val_rel_cons .
rewrite <- sem_val_rel_cons .
exact v'_log .
}
(* We can deduce from v₁ ∈ 𝒱 ( v' ) in τ, it will step to a value in τ₂ *)
simp type_interp in v ₂ _ in_Bfn .
destruct v ₂ _ in_Bfn as ( x ₂ & e' & -> & e ₁ _ cl & v ₂ _ ty ) .
specialize ( v ₂ _ ty v' v'_in_B' ) .
simp type_interp in v ₂ _ ty .
destruct v ₂ _ ty as [ v ₂ ' [ v ₂ _ bs v ₂ ' _ ty ] ] .
simp type_interp .
eexists ; split .
(* We can see that our if-expression steps to ( v₂ v' ) *)
bs_step_det .
eapply bs_if_false .
bs_step_det .
econstructor .
apply big_step_of_val ; reflexivity .
bs_step_det .
(* So we can use the information from v₂ ∈ 𝒱 *)
exact v ₂ _ bs .
exact v ₂ ' _ ty .
Qed .
End ex5 .
@ -159,11 +497,278 @@ Proof.
all : asimpl ; solve_typing .
Qed .
Ltac 𝒱 2_ λ := simp type_interp ; eexists ; eexists ; eexists ; eexists ;
split ; last split ; last split ; last split ;
[ reflexivity | reflexivity | simplify_closed | simplify_closed | ]
.
Ltac 𝒱 2_ inner :=
simp type_interp ; eexists ; eexists ; split ; last split ; simpl ;
[ try bs_step_det | try bs_step_det | ]
.
(*
I consider this to be an example of bad pedagogy .
This is more of a challenge than an exercise ; I didn't learn anything proving this ,
and all it brought to me was a net loss in energy and a lot of frustration .
This is the kind of theorem that should be proven automatically ,
and we have constructed in class the tools needed to implement such a prover ,
we just chose not to make one and to instead spearhead our way into proving this kind of stuff ,
by hand .
The ` destruct ` forests , the stacked ` split ` s , the ` eexists ` spam are witnesses that proving this is a bad idea , and that asking students to prove this is a bad idea .
I spent 30 seconds writing the definition of τ , and 1 hour proving the rest of the theorem .
* )
Lemma sum_ex_impl_equiv n Γ A B :
ctx_equiv n Γ sum_ex_impl' sum_ex_impl ( sum_ex_type A B ) .
Proof .
(* TODO: exercise *)
Admitted .
(*
To prove that sum_ex_impl' = = = _ ctx sum_ex_impl ,
we can prove that n ; Γ | = sum_ex_impl ~ sum_ex_impl' : SUM ( A , B )
* )
apply sem_typing_ctx_equiv .
simplify_closed .
simplify_closed .
split ; last split .
simplify_closed .
simplify_closed .
intros θ 1 θ 2 δ Hctx .
destruct ( sem_context_rel_closed _ _ _ _ Hctx ) as [ Hcl1 Hcl2 ] .
simp type_interp .
eexists ; eexists ; split ; last split .
bs_step_det .
bs_step_det .
(* Clean up our expression *)
repeat rewrite lookup_delete .
have h ₁ : delete " f2 " ( delete " f1 " ( delete " x " θ 1 ) ) !! " x " = None .
{
rewrite lookup_delete_ne .
rewrite lookup_delete_ne .
apply lookup_delete .
eauto .
eauto .
}
rewrite h ₁ .
have h ₂ : delete " f2 " ( delete " f1 " ( delete " x " θ 2 ) ) !! " x " = None .
{
rewrite lookup_delete_ne .
rewrite lookup_delete_ne .
apply lookup_delete .
eauto .
eauto .
}
rewrite h ₂ .
have h ₃ : delete " f2 " ( delete " f1 " ( delete " x " θ 1 ) ) !! " f1 " = None .
{
rewrite lookup_delete_ne .
apply lookup_delete .
eauto .
}
rewrite h ₃ .
have h ₄ : delete " f2 " ( delete " f1 " ( delete " x " θ 2 ) ) !! " f1 " = None .
{
rewrite lookup_delete_ne .
apply lookup_delete .
eauto .
}
rewrite h ₄ .
unfold sum_ex_type .
simp type_interp ; eexists ; eexists ; split ; first reflexivity ; split ; first reflexivity .
remember ( λ v1 v2 , match v1 , v2 with
| ( InjLV x ) , ( PairV ( LitV ( LitInt 1 ) ) y ) => 𝒱 A δ x y
| ( InjRV x ) , ( PairV ( LitV ( LitInt 2 ) ) y ) => 𝒱 B δ x y
| _ , _ => False
end
) as τ _ λ .
(* Please look away *)
have inv_ τ : ∀ v1 v2 , τ _ λ v1 v2 → ∃ x y ,
(
v1 = ( InjLV x )
∧ v2 = ( PairV ( LitV ( LitInt 1 ) ) y )
∧ 𝒱 A δ x y
)
∨ (
v1 = ( InjRV x )
∧ v2 = ( PairV ( LitV ( LitInt 2 ) ) y )
∧ 𝒱 B δ x y
) .
{
intros v1 v2 v_in_ τ .
rewrite Heq τ _ λ in v_in_ τ .
destruct v1 ; try ( exfalso ; exact v_in_ τ ) .
{
destruct v2 ; try ( exfalso ; exact v_in_ τ ) .
destruct v2_1 ; try ( exfalso ; exact v_in_ τ ) .
destruct l ; try ( exfalso ; exact v_in_ τ ) .
destruct n0 ; try ( exfalso ; exact v_in_ τ ) .
destruct p ; try ( exfalso ; exact v_in_ τ ) .
eexists ; eexists .
left .
split ; last split .
reflexivity .
reflexivity .
assumption .
}
{
destruct v2 ; try ( exfalso ; exact v_in_ τ ) .
destruct v2_1 ; try ( exfalso ; exact v_in_ τ ) .
destruct l ; try ( exfalso ; exact v_in_ τ ) .
destruct n0 ; try ( exfalso ; exact v_in_ τ ) .
destruct p ; try ( exfalso ; exact v_in_ τ ) .
destruct p ; try ( exfalso ; exact v_in_ τ ) .
eexists ; eexists .
right .
split ; last split .
reflexivity .
reflexivity .
assumption .
}
}
pose_sem_type τ _ λ as τ .
{
intros v w vw_in_ τ .
destruct ( inv_ τ v w vw_in_ τ ) as ( v' & w' & [ ( -> & -> & He ) | ( -> & -> & He ) ] ) .
simplify_closed .
destruct ( val_rel_is_closed _ _ _ _ He ) as [ Hcl3 Hcl4 ] .
split ; assumption .
simplify_closed .
destruct ( val_rel_is_closed _ _ _ _ He ) as [ Hcl3 Hcl4 ] .
split ; assumption .
}
exists τ .
simp type_interp ; eexists ; eexists ; eexists ; eexists ; split ; first reflexivity ; split ; first reflexivity ; split .
simp type_interp ; eexists ; eexists ; eexists ; eexists ; split ; first reflexivity ; split ; first reflexivity ; split .
- 𝒱 2_ λ .
intros v w vw_in_ τ .
𝒱 2_ inner .
simp type_interp .
simpl .
rewrite Heq τ _ λ .
rewrite <- sem_val_rel_cons in vw_in_ τ .
assumption .
- 𝒱 2_ λ .
intros v w vw_in_ τ .
𝒱 2_ inner .
simp type_interp .
simpl .
rewrite Heq τ _ λ .
rewrite <- sem_val_rel_cons in vw_in_ τ .
assumption .
- simp type_interp .
eexists ; eexists ; split ; last split ; last split ; last split ; [ reflexivity | reflexivity | simplify_closed | simplify_closed | ] .
intro τ ₂ .
simp type_interp ; eexists ; eexists ; split ; last split ; [ bs_step_det | bs_step_det | ] .
𝒱 2_ λ .
intros v w vw_in_ τ .
𝒱 2_ inner .
destruct ( val_rel_is_closed _ _ _ _ vw_in_ τ ) as [ Hcl3 Hcl4 ] .
simp type_interp in vw_in_ τ ; simpl in vw_in_ τ .
𝒱 2_ λ .
intros f1 f1' f1_in_ τ ₂ .
𝒱 2_ inner .
destruct ( val_rel_is_closed _ _ _ _ f1_in_ τ ₂ ) as [ Hcl5 Hcl6 ] .
𝒱 2_ λ .
intros f2 f2' f2_in_ τ ₂ .
destruct ( inv_ τ v w vw_in_ τ ) as ( v' & w' & [ ( -> & -> & He ) | ( -> & -> & He ) ] ) ;
destruct ( val_rel_is_closed _ _ _ _ He ) as [ Hcl9 Hcl10 ] ;
destruct ( val_rel_is_closed _ _ _ _ f2_in_ τ ₂ ) as [ Hcl7 Hcl8 ] .
+
repeat rewrite subst_is_closed_nil ; try assumption .
simp type_interp in f1_in_ τ ₂ .
destruct f1_in_ τ ₂ as ( x1 & x1' & f1_body & f1'_body & Heq_f1body & Heq_f1'body & Hcl11 & Hcl12 & Hlog ) .
have HA : 𝒱 A . [ ren ( + 2 ) ] ( τ ₂ . : τ . : δ ) v' w' .
{
rewrite ren_2 .
rewrite <- sem_val_rel_cons .
rewrite <- sem_val_rel_cons .
assumption .
}
specialize ( Hlog v' w' HA ) .
simp type_interp in Hlog .
destruct Hlog as ( v1 & v1' & Hbs & Hbs' & Hlog ) .
simp type_interp .
exists v1 .
exists v1' .
split ; last split .
simpl .
repeat ( rewrite subst_is_closed_nil ; last assumption ) .
econstructor .
econstructor ; apply big_step_of_val ; reflexivity .
econstructor ; try ( apply big_step_of_val ; reflexivity ) .
apply big_step_of_val . rewrite Heq_f1body ; reflexivity .
assumption .
simpl .
repeat ( rewrite subst_is_closed_nil ; last assumption ) .
econstructor .
bs_step_det .
econstructor .
apply big_step_of_val . rewrite Heq_f1'body ; reflexivity .
bs_step_det .
assumption .
assumption .
+ repeat rewrite subst_is_closed_nil ; try assumption .
simp type_interp in f2_in_ τ ₂ .
destruct f2_in_ τ ₂ as ( x2 & x2' & f2_body & f2'_body & Heq_f2body & Heq_f2'body & Hcl11 & Hcl12 & Hlog ) .
have HB : 𝒱 B . [ ren ( + 2 ) ] ( τ ₂ . : τ . : δ ) v' w' .
{
rewrite ren_2 .
rewrite <- sem_val_rel_cons .
rewrite <- sem_val_rel_cons .
assumption .
}
specialize ( Hlog v' w' HB ) .
simp type_interp in Hlog .
destruct Hlog as ( v2 & v2' & Hbs & Hbs' & Hlog ) .
simp type_interp .
exists v2 .
exists v2' .
split ; last split .
simpl .
repeat ( rewrite subst_is_closed_nil ; last assumption ) .
eapply bs_caser .
econstructor ; apply big_step_of_val ; reflexivity .
econstructor ; try ( apply big_step_of_val ; reflexivity ) .
apply big_step_of_val . rewrite Heq_f2body ; reflexivity .
assumption .
simpl .
repeat ( rewrite subst_is_closed_nil ; last assumption ) .
eapply bs_if_false .
bs_step_det .
econstructor .
apply big_step_of_val . rewrite Heq_f2'body ; reflexivity .
bs_step_det .
assumption .
assumption .
Qed .
End ex8 .
