ImpAlg.ImplicativeAlgebras
Set Implicit Arguments.
Set Contextual Implicit.
Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Import Relation_Definitions.
Require Import TLC.LibLN.
Require Import Arith.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.ImplicativeStructures.
Require Import Sets.Ensembles.
Require Import ImpAlg.Lambda.
Require Import ImpAlg.Adequacy.
Require Import ImpAlg.Combinators.
Set Contextual Implicit.
Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Import Relation_Definitions.
Require Import TLC.LibLN.
Require Import Arith.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.ImplicativeStructures.
Require Import Sets.Ensembles.
Require Import ImpAlg.Lambda.
Require Import ImpAlg.Adequacy.
Require Import ImpAlg.Combinators.
Class ImplicativeAlgebra `{IS:ImplicativeStructure}:=
{
separator: X → Prop;
modus_ponens: ∀ a b, separator a → separator (arrow a b) → separator b;
up_closed: ∀ a b, ord a b → separator a → separator b;
sep_K : separator K;
sep_S : separator S;
sep_cc : separator cc
}.
Generalizable Variables separator.
Notation "a ∈ʆ":= (separator a) (at level 80,no associativity).
Infix "@" := (app) (at level 59, left associativity).
Notation "λ- f":= (abs f) (at level 60).
Hint Resolve arrow_meet modus_ponens sep_K sep_S sep_cc.
Hint Unfold arrow_set_l arrow_set_r arrow_set.
Section IA.
Context `{IA:ImplicativeAlgebra}.
Definition env:=@env X.
Definition codom:=@codom X.
Definition fv_trm:=@fv_trm X.
Definition fv_typ:=@fv_typ X.
A convenient notation for λ-terms.
Notation "λ+ t":= (trm_abs (t)) (at level 69, right associativity).
Notation "[ t ] u":= (trm_app (t) u ) (at level 69, right associativity).
Notation "$ n":= (@trm_bvar X n) (at level 69, right associativity).
Definition neg a:=a ↦ ⊥.
Definition closed_typ (T:typ):= fv_typ T = \{}.
We define again the tactis to pick fresh variables.
Ltac gather_vars :=
let A := gather_vars_with (fun x : vars => x) in
let B := gather_vars_with (fun x : var => \{x}) in
let C := gather_vars_with (fun x : env => (dom x)\u (codom x)) in
let D := gather_vars_with (fun x : trm => fv_trm x) in
let E := gather_vars_with (fun x : typ => fv_typ x) in
constr:(A \u B \u C \u D \u E).
Ltac pick_fresh Y :=
let L := gather_vars in (pick_fresh_gen L Y).
Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
apply_fresh_base T gather_vars x.
Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
apply_fresh T as x; auto_star.
Tactic Notation "apply_fresh" constr(T) :=
apply_fresh_base T gather_vars ltac_no_arg.
Tactic Notation "apply_fresh" "*" constr(T) :=
apply_fresh T; auto_star.
let A := gather_vars_with (fun x : vars => x) in
let B := gather_vars_with (fun x : var => \{x}) in
let C := gather_vars_with (fun x : env => (dom x)\u (codom x)) in
let D := gather_vars_with (fun x : trm => fv_trm x) in
let E := gather_vars_with (fun x : typ => fv_typ x) in
constr:(A \u B \u C \u D \u E).
Ltac pick_fresh Y :=
let L := gather_vars in (pick_fresh_gen L Y).
Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
apply_fresh_base T gather_vars x.
Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
apply_fresh T as x; auto_star.
Tactic Notation "apply_fresh" constr(T) :=
apply_fresh_base T gather_vars ltac_no_arg.
Tactic Notation "apply_fresh" "*" constr(T) :=
apply_fresh T; auto_star.
We define a simple tactic to automatize the proof that a pre-term is a term,
when it is the case.
Ltac fresh_term_abs :=
let L0:=gather_vars in let L1 := beautify_fset L0 in
apply (@term_abs _ L1);intros.
Ltac fresh_sterm_abs :=
let L0:=gather_vars in let L1 := beautify_fset L0 in
apply (@sterm_abs _ L1);intros.
Ltac fresh_typing_abs :=
let L0:=gather_vars in let L1 := beautify_fset L0 in
apply (@typing_abs _ L1);intros.
Ltac autosterm :=
repeat (
try (apply sterm_cc);try (apply sterm_var);try (fresh_sterm_abs);
try (apply sterm_app);try (unfold Succ);try (case_nat);try (cbn)
).
Bunch of tactics to automatize typing, etc..
Ltac autofv := cbn;repeat (try rewrite union_empty_l;try rewrite union_empty_r);reflexivity.
Ltac autosclosed:=split;[autosterm|autofv].
Ltac translated_sclosed:=split;[find_translated|autosclosed].
Ltac exists_sterm t:= exists t;translated_sclosed.
Ltac autoclosed_typ:=unfold closed_typ;cbn;repeat (rewrite union_empty_l);auto.
Ltac typ_from_translated:=
unfold neg;
repeat (
match goal with
| |- translated_typ _ (⊓ (_)) => apply tr_typ_fall;intros
| |- translated_typ _ (_ ↦ _) => apply tr_typ_arrow
| |- translated_typ _ ?a => apply tr_typ_var
end
).
Ltac autotype :=
repeat (
try (apply type_fvar);try (apply type_cvar);
try (apply_fresh type_fall);try (apply type_arrow)
).
Ltac simplIf:=repeat (try (rewrite If_l;[|reflexivity]);try (rewrite If_r;[|auto])).
Ltac autoget:=
repeat(
match goal with
| |- _ # _ => apply get_none_inv
| |- get _ EnvOps.empty = None => apply get_empty
| |- get _ (_ & _ ) = None => rewrite get_push;simplIf
end
).
Ltac autook:=repeat (apply ok_push);try (rewrite <- empty_eq);try (apply ok_empty); autoget.
Ltac autobinds:=
match goal with
| |- binds ?y _ (?E & ?y ~ _) => apply* binds_push_eq
| |- binds ?y _ (?E & ?z ~ _) => apply* binds_push_neq
end.
Ltac autotyping:=
repeat (
match goal with
| H: _ \notin _ \u _ |- _ => rewrite_all notin_union in *
| H: _ \notin \{_} |- _ => rewrite_all notin_singleton in *
| H: _ \notin \{} |- _ => clear H
| H: _ ∧ _ |- _ => destruct H
| |- ok _ => autook
| |- typing_trm _ (λ+ _) (typ_arrow _ _) => fresh_typing_abs;autotype;unfold open_trm;simpl;simplIf
| |- typing_trm _ ([ _ ] _ ) _ => eapply typing_app
| |- typing_trm _ (trm_fvar _) ?a => apply typing_prf_var;[autook|autobinds|autotype]
| |- type _ => autotype
end
).
Ltac exX a:=exists (a X).
Lemma app_closed : ∀ a b, a ∈ʆ → b ∈ʆ → a@b ∈ʆ.
Proof.
intros.
apply (modus_ponens b (a@b)).
- assumption.
- apply (up_closed a).
+ apply adjunction.
apply ord_refl.
+ assumption.
Qed.
We show that any separator contains the interpretation of all (strictly) closed λ-terms.
Hint Resolve sep_S sep_K.
Lemma sep_Id: Id ∈ʆ.
Proof.
apply (up_closed _ _ Id_SK).
repeat (apply app_closed);auto.
Qed.
Hint Resolve sep_Id.
Any combinator belongs to the separator
Lemma sep_comb: ∀ A, combinator A → A ∈ʆ.
Proof.
intros.
induction H;auto.
apply app_closed;auto.
Qed.
Proof.
intros.
induction H;auto.
apply app_closed;auto.
Qed.
Any sclosed term which has a translated is in the separator
Lemma sep_term: ∀ C, (exists t, translated t C ∧ sclosed t) → C ∈ʆ.
Proof.
intros C (t,(Tr,Clo)).
destruct (combinator_trm_translated Clo Tr) as (c,(Comb,Hc)).
apply (up_closed c);trivial.
now apply sep_comb.
Qed.
Any strictly closed term has a translated element
Lemma sclosed_translated_n: ∀n t σ, size t <= n → closed t → translated t (trans_trm σ t).
Proof.
intros n; induction n;
intros t σ Size [Sterm FV];[exfalso;now apply (size_not_0 t)|].
destruct t;simpl in *;(try inversion Sterm);auto.
- exfalso. rewrite<- (in_empty a).
rewrite <- FV. now rewrite in_singleton.
- cbn. apply tr_cvar.
- rewrite trans_trm_abs.
apply tr_abs;intros.
apply IHn.
+ unfold open_trm. rewrite size_open_c;auto with arith.
+ split.
* apply open_trm_term. unfold body. exists L0;auto. apply term_cvar.
* unfold open_trm;now rewrite fv_trm_subst.
- apply union_empty in FV as (FV1,FV2).
rewrite trans_trm_app. apply tr_app.
+ apply IHn. now apply size_app_le_l with t2.
split;auto.
+ apply IHn. now apply size_app_le_r with t1.
split;auto.
- cbn;apply tr_cc.
Qed.
Lemma sclosed_translated: ∀t σ, sclosed t → translated t (trans_trm σ t).
Proof.
intros t σ H. apply sclosed_translated_n with (size t);auto.
split;destruct H;auto. now apply sterm_term.
Qed.
Proof.
intros n; induction n;
intros t σ Size [Sterm FV];[exfalso;now apply (size_not_0 t)|].
destruct t;simpl in *;(try inversion Sterm);auto.
- exfalso. rewrite<- (in_empty a).
rewrite <- FV. now rewrite in_singleton.
- cbn. apply tr_cvar.
- rewrite trans_trm_abs.
apply tr_abs;intros.
apply IHn.
+ unfold open_trm. rewrite size_open_c;auto with arith.
+ split.
* apply open_trm_term. unfold body. exists L0;auto. apply term_cvar.
* unfold open_trm;now rewrite fv_trm_subst.
- apply union_empty in FV as (FV1,FV2).
rewrite trans_trm_app. apply tr_app.
+ apply IHn. now apply size_app_le_l with t2.
split;auto.
+ apply IHn. now apply size_app_le_r with t1.
split;auto.
- cbn;apply tr_cc.
Qed.
Lemma sclosed_translated: ∀t σ, sclosed t → translated t (trans_trm σ t).
Proof.
intros t σ H. apply sclosed_translated_n with (size t);auto.
split;destruct H;auto. now apply sterm_term.
Qed.
Proposition 28: the intepretation of any sclosed term is in the separator.
Lemma sep_sclosed: ∀ t, sclosed t → ∀ σ, (trans_trm σ t) ∈ʆ.
Proof.
intros t H σ. apply sep_term. exists t;split;auto;now apply sclosed_translated.
Qed.
Proof.
intros t H σ. apply sep_term. exists t;split;auto;now apply sclosed_translated.
Qed.
Corollary 29: the interpretation of any type T s.t. there exists
a sclosed term t of type T belongs to the separator.
Lemma sep_typ:
∀ C, (exists t T, translated_typ T C ∧ closed_typ T ∧ sclosed t ∧ typing_trm empty t T) → C ∈ʆ.
Proof.
intros C (t,(T,(Tr,(Cl,(Scl,Typ))))).
destruct (translated_closed (typing_empty_closed Typ)) as (a,Ha).
apply (up_closed a).
apply (adequacy_empty Typ Ha Cl Tr).
apply sep_term. exists t; auto.
Qed.
In particular, the following terms belong to the separator
Lemma sep_W: W ∈ʆ.
Proof.
apply sep_term.
exX @lambdaW.
split.
apply translated_W.
autosclosed.
Qed.
Lemma sep_Easy: Easy ∈ʆ.
Proof.
apply sep_term.
exX @lambdaEasy.
split.
apply translated_Easy.
autosclosed.
Qed.
Hint Resolve sep_Id sep_W sep_Easy.
Proof.
apply sep_term.
exX @lambdaW.
split.
apply translated_W.
autosclosed.
Qed.
Lemma sep_Easy: Easy ∈ʆ.
Proof.
apply sep_term.
exX @lambdaEasy.
split.
apply translated_Easy.
autosclosed.
Qed.
Hint Resolve sep_Id sep_W sep_Easy.
Definition entails a b := (a ↦ b) ∈ʆ .
Infix "⊢":= entails (at level 75).
Definition equivalence a b := a ⊢ b ∧ b ⊢ a.
Infix "≈":= equivalence (at level 80).
Notation "¬ a":=(neg a).
The ordering relation is including in the entailment relation Proposition 32.3
Lemma subtyping : ∀ a b, a ≤ b → a ⊢ b.
Proof.
intros.
apply (up_closed (a ↦ a)).
+ apply arrow_mon_r.
assumption.
+ apply (up_closed (Id)); auto.
apply meet_elim. exists a;reflexivity.
Qed.
Proof.
intros.
apply (up_closed (a ↦ a)).
+ apply arrow_mon_r.
assumption.
+ apply (up_closed (Id)); auto.
apply meet_elim. exists a;reflexivity.
Qed.
We define a tactic "realizer" to automatize to proof
that a given a∈A element belongs to the separator.
This tactics takes a λ-terms t as input and try to show that t ≤ a.
It might go to far in trying to find the translation of t,
in which case realizer_step is useful.
Lemma realizer_later: ∀ a, (exists b, b ∈ʆ ∧ b ≤ a) → a ∈ʆ.
Proof.
intros a (b,(Hb,Ha)).
apply (modus_ponens b _ Hb).
apply* (subtyping).
Qed.
Ltac in_sep_sterm t:= apply sep_term;exists t;split;[find_translated|autosclosed].
Ltac emeet_elim:=apply (meet_elim_trans);later;split;[later;reflexivity|].
Ltac hnform:=repeat (emeet_elim;apply arrow_mon_r);adjunction_mon.
Ltac realizer t:= apply realizer_later;later;split;[in_sep_sterm t| hnform].
Ltac realizer_step t:= apply realizer_later;later;split;[in_sep_sterm t|].
We illustrate the utility of this tactic on a simple example (Rmk 30)
Lemma composition: ∀ a b c, (a ↦ b) ↦ (b ↦ c) ↦ (a ↦ c) ∈ʆ.
Proof. intros. realizer ((λ+ λ+ λ+ ([ $ 1 ] ([$ 2] $ 0)))). Qed.
λxyz.y(xz)
The entailment relation is a preorder
Proposition 32.1
Lemma entails_refl : reflexive X entails.
Proof.
unfold entails,reflexive.
intro a.
realizer (λ+ $0).
Qed.
Proof.
unfold entails,reflexive.
intro a.
realizer (λ+ $0).
Qed.
Proposition 32.2
Lemma entails_trans : transitive X entails.
Proof.
unfold entails,transitive.
intros a b c Ha Hb.
apply (modus_ponens (b ↦ c));auto.
apply (modus_ponens (a ↦ b));auto.
realizer (λ+ λ+ λ+ ([$1] ([$2] $0))).
Qed.
Proof.
unfold entails,transitive.
intros a b c Ha Hb.
apply (modus_ponens (b ↦ c));auto.
apply (modus_ponens (a ↦ b));auto.
realizer (λ+ λ+ λ+ ([$1] ([$2] $0))).
Qed.
Proposition 32.4
Lemma equiv_sep: ∀ a b, a ≈ b → (a ∈ʆ ↔ b ∈ʆ).
Proof.
intros a b (Hab,Hba).
split;intro H;
[apply (modus_ponens _ _ H Hab)|
apply (modus_ponens _ _ H Hba)].
Qed.
Proof.
intros a b (Hab,Hba).
split;intro H;
[apply (modus_ponens _ _ H Hab)|
apply (modus_ponens _ _ H Hba)].
Qed.
Proposition 32.5
Lemma entails_half_adj:
∀a b c, a ⊢ b ↦ c → a ⋀ b ⊢ c .
Proof.
intros a b c H.
apply modus_ponens with (a0:=a ↦ b ↦ c);auto.
apply (up_closed W);auto. unfold W.
apply (ord_trans _ (((a ⋀ b) ↦ (a ⋀ b) ↦ c) ↦ (a ⋀ b) ↦ c)).
- auto_meet_elim_trans.
- repeat apply arrow_mon;intuition.
Qed.
Lemma mod_ponens : ∀ a b, (a ↦ b) ⋀ a ⊢ b.
Proof.
intros.
apply entails_half_adj.
apply entails_refl.
Qed.
Lemma modus_ponens_later: ∀ a, (exists b, b ∈ʆ ∧ b ⊢ a ) → a ∈ʆ.
Proof.
intros a (b,(Hb,Ha)).
apply* (modus_ponens b).
Qed.
∀a b c, a ⊢ b ↦ c → a ⋀ b ⊢ c .
Proof.
intros a b c H.
apply modus_ponens with (a0:=a ↦ b ↦ c);auto.
apply (up_closed W);auto. unfold W.
apply (ord_trans _ (((a ⋀ b) ↦ (a ⋀ b) ↦ c) ↦ (a ⋀ b) ↦ c)).
- auto_meet_elim_trans.
- repeat apply arrow_mon;intuition.
Qed.
Lemma mod_ponens : ∀ a b, (a ↦ b) ⋀ a ⊢ b.
Proof.
intros.
apply entails_half_adj.
apply entails_refl.
Qed.
Lemma modus_ponens_later: ∀ a, (exists b, b ∈ʆ ∧ b ⊢ a ) → a ∈ʆ.
Proof.
intros a (b,(Hb,Ha)).
apply* (modus_ponens b).
Qed.
This example is only given to illustrate the utility of some tactics.
Actually, this formula is realized by λxyz.y(xz) and the following is enough
to prove the lemma:
realizer ((λ+ λ+ λ+ ( $ 1 ($ 2
Lemma contraposition_l: ∀ a b, a ↦ b ⊢ (¬ b) ↦ ¬ a.
Proof.
intros.
unfold entails,neg.
(* realizer ((λ+ λ+ λ+ ( $ 1 ($ 2 *)
apply sep_typ.
exists ((λ+ λ+ λ+ ([ $ 1 ] ([$ 2] $ 0)))).
later.
split;[typ_from_translated|].
split;[autoclosed_typ|].
split;[autosclosed|].
autotyping.
Qed.
Ex falso quod libet: Proposition 32.6
⊤ is the maximal element Proposition 32.7
Lemma dni: ∀ a, a ⊢ ¬ (¬ a).
Proof.
intro. unfold neg.
realizer (λ+ λ+ ([$0] $1)).
Qed.
Lemma dne: ∀ a, (¬ (¬ a)) ⊢ a.
Proof.
intro. unfold entails,neg.
apply (up_closed (((a ↦ ⊥ ) ↦ a) ↦ a)).
- adjunction_mon.
- apply (up_closed cc);auto.
auto_meet_elim_trans.
Qed.
Lemma dn: ∀ a, a ≈ ¬ ¬ a.
Proof.
intros;split;[apply dni|apply dne].
Qed.
The relation of entailment is compatible with the arrow:
Proposition 33
Lemma arrow_entails_mon_r: ∀ a b b', b ⊢ b' → a ↦ b ⊢ a ↦ b'.
Proof.
intros a b b' H.
apply modus_ponens_later. exists (b ↦ b'). split;auto.
realizer (λ+ λ+ λ+ ([ $2 ] ([ $1 ] $0))).
Qed.
Lemma arrow_entails_mon_l: ∀ a a' b, a ⊢ a' → a' ↦ b ⊢ a ↦ b.
Proof.
intros a a' b H.
apply modus_ponens_later. exists (a ↦ a'). split;auto.
realizer (λ+ λ+ λ+ ([ $1 ] ([ $2 ] $0))).
Qed.
Lemma arrow_entails_mon: ∀ a a' b b', a' ⊢ a → b ⊢ b' → a ↦ b ⊢ a' ↦ b'.
Proof.
intros a a' b b' Ha Hb.
apply modus_ponens_later. exists (b ↦ b'). split;auto.
apply modus_ponens_later. exists (a' ↦ a). split;auto.
realizer (λ+ λ+ λ+ λ+ ([ $2 ] ([ $1 ] ([ $3 ] $0)))).
Qed.
Lemma contraposition_r: ∀ a b, (¬ a) ↦ (¬ b) ⊢ b ↦ a.
Proof.
intros.
apply (@entails_trans ((¬ a) ↦ ¬ b) ((¬ ¬ b) ↦ ¬ ¬ a)).
- apply contraposition_l.
- apply arrow_entails_mon.
+ apply dni.
+ apply dne.
Qed.
Proof.
intros a b b' H.
apply modus_ponens_later. exists (b ↦ b'). split;auto.
realizer (λ+ λ+ λ+ ([ $2 ] ([ $1 ] $0))).
Qed.
Lemma arrow_entails_mon_l: ∀ a a' b, a ⊢ a' → a' ↦ b ⊢ a ↦ b.
Proof.
intros a a' b H.
apply modus_ponens_later. exists (a ↦ a'). split;auto.
realizer (λ+ λ+ λ+ ([ $1 ] ([ $2 ] $0))).
Qed.
Lemma arrow_entails_mon: ∀ a a' b b', a' ⊢ a → b ⊢ b' → a ↦ b ⊢ a' ↦ b'.
Proof.
intros a a' b b' Ha Hb.
apply modus_ponens_later. exists (b ↦ b'). split;auto.
apply modus_ponens_later. exists (a' ↦ a). split;auto.
realizer (λ+ λ+ λ+ λ+ ([ $2 ] ([ $1 ] ([ $3 ] $0)))).
Qed.
Lemma contraposition_r: ∀ a b, (¬ a) ↦ (¬ b) ⊢ b ↦ a.
Proof.
intros.
apply (@entails_trans ((¬ a) ↦ ¬ b) ((¬ ¬ b) ↦ ¬ ¬ a)).
- apply contraposition_l.
- apply arrow_entails_mon.
+ apply dni.
+ apply dne.
Qed.
We define simple tactics to automatize the proof by beta reduction
for goals of the shape λ- f ≤ a ↦ b or λ- f ≤ ⋂_ t
Ltac lam_leq:=apply adjunction,beta_red;try (adjunction_mon).
Ltac lam_meet:=auto_meet_intro;apply adjunction,beta_red.
Definition forallt:=meet_family.
Definition existst `{I:Type} (a:I→X):=⋂[c](meet_family (fun (i:I)=> a i ↦ c) ↦ c).
Definition ex_term t := λ- (fun x => x@t).
Notation "[∀] a":=(forallt a) (at level 69).
Notation "[∃] a":=(existst a) (at level 69).
Proposition 35: We prove the semantic typing rules for the ∀ type
Lemma type_fa_intro:
∀ I (a:I→X) t, (∀ i, t ≤ a i) → t ≤ [∀] a.
Proof.
intros I a t H.
now auto_meet_intro.
Qed.
Lemma type_fa_elim:
∀ I (a:I→X) t, t ≤ [∀] a → ∀i, t≤ a i.
Proof.
intros I a t H i.
eapply ord_trans;[exact H|].
auto_meet_elim_trans.
Qed.
Proposition 36: We prove the semantic typing rules for the ∃ type
Lemma type_ex_intro:
∀ I (a:I→X) t, (∃ i, t ≤ a i) → λ- (fun x => x@t) ≤ [∃] a.
Proof.
intros I a t [i H].
lam_meet.
apply adjunction.
auto_meet_elim_trans.
apply arrow_mon_l;exact H.
Qed.
Lemma type_ex_elim:
∀ I (a:I→X) t u c, t ≤ [∃] a → (∀i x, x≤ a i → u x≤ c) → (t@λ- (fun x => u x))≤ c.
Proof.
intros I a t u c H Hu.
apply adjunction. eapply ord_trans;[exact H|].
auto_meet_elim_trans. apply arrow_mon_l.
apply meet_intro. intros x [i Hx]. subst.
lam_leq. now apply (Hu i).
Qed.
Definition prodt a b :=(⋂[c] ((a ↦ b ↦ c) ↦c)).
Notation "a × b":=(prodt a b) (at level 69).
Definition pair a b :=λ- (fun x => x@ a @ b).
Definition proj1:= λ- (fun x => λ- (fun y => x)).
Definition proj2:= λ- (fun x => λ- (fun y => y)).
Proposition 37: We prove the semantic typing rules for the × type
Lemma type_pair:
∀ a b t u, t ≤ a → u ≤ b → pair t u ≤ a × b .
Proof.
intros a b t u Ha Hb.
apply meet_intro.
intros x [c H]. subst.
lam_leq.
do 2 apply adjunction.
do 2 (apply arrow_mon;intuition).
Qed.
Lemma type_proj1:
∀ a b t , t ≤ a × b → t@proj1 ≤ a.
Proof.
intros a b t Ha.
apply adjunction.
eapply ord_trans;[exact Ha|].
auto_meet_elim_trans. apply arrow_mon_l.
now do 2 lam_leq.
Qed.
Lemma type_proj2:
∀ a b t , t ≤ a × b → t@proj2 ≤ b.
Proof.
intros a b t Ha.
apply adjunction.
eapply ord_trans;[exact Ha|].
auto_meet_elim_trans. apply arrow_mon_l.
now do 2 lam_leq.
Qed.
Proposition 39: We prove the adjunction for × and ↦ in the induced Heyting prealgebra
Lemma ha_adjunction:
∀ a b c, a ⊢ b ↦ c <-> a × b ⊢ c.
Proof.
intros a b c;split;intro H.
- apply modus_ponens_later.
exists (a ↦ b ↦ c);split;auto.
realizer (λ+ λ+ [$0] $1).
apply adjunction.
auto_meet_elim_trans.
- apply modus_ponens_later.
exists ((a × b) ↦ c);split;auto.
unfold entails.
realizer_step (λ+ λ+ λ+ [$2] (λ+ ([[$0] $2] $1))).
do 3 lam_leq.
lam_meet.
apply adjunction. adjunction_mon.
Qed.
We prove that × is indeed a meet in the induced Heyting prealgebra:
Lemma prodt_l:
∀ a b, a × b ⊢ a.
Proof.
intros a b.
realizer (λ+ [$0] (λ+ λ+ $1)).
apply adjunction.
auto_meet_elim_trans. apply arrow_mon_l.
now do 2 lam_leq.
Qed.
Lemma prodt_r:
∀ a b, a × b ⊢ b.
Proof.
intros a b.
realizer (λ+ [$0] (λ+ λ+ $0)).
apply adjunction.
auto_meet_elim_trans. apply arrow_mon_l.
now do 2 lam_leq.
Qed.
Lemma prodt_intro:
∀ a b c, c ⊢ a → c ⊢ b → c ⊢ a × b.
Proof.
intros a b c Ha Hb.
apply modus_ponens with (a0:=c↦b);auto.
apply modus_ponens with (a0:=c↦a);auto.
(* λtucz.z(tc)(uc) *)
realizer (λ+ λ+ λ+ λ+ [[$0] ([$3] $1)] ([$2] $1)).
lam_meet.
do 2 apply adjunction.
apply arrow_mon;adjunction_mon.
Qed.
Definition sumt a b :=(⋂[c] ((a ↦ c) ↦ (b ↦ c) ↦c)).
Notation "a ⊕ b":=(sumt a b) (at level 69).
Definition inj1 t:= λ- (fun x => λ- (fun y => x@t )).
Definition inj2 t:= λ- (fun x => λ- (fun y => y@t)).
Definition case t u v := (t@λ- (fun x => u x)) @ λ- (fun x => v x).
Proposition 38: We prove the semantic typing rules for the + type
Lemma type_inj1:
∀ a b t , t ≤ a → inj1 t ≤ a ⊕ b.
Proof.
intros a b t Ha.
lam_meet. lam_leq.
Qed.
Lemma type_inj2:
∀ a b t , t ≤ b → inj2 t ≤ a ⊕ b.
Proof.
intros a b t Ha.
lam_meet. lam_leq.
Qed.
Lemma type_case:
∀ a b c t u v, t ≤ a ⊕ b → (∀x,x≤a → u x≤ c) → (∀x,x≤b → v x≤ c)
→ case t u v ≤ c.
Proof.
intros a b c t u v Ht Hu Hv.
do 2 apply adjunction.
eapply ord_trans;[exact Ht|].
auto_meet_elim_trans.
apply arrow_mon;[|apply arrow_mon_l];lam_leq;intuition.
Qed.
We prove that + is indeed a join in the induced Heyting prealgebra:
Lemma sumt_l:
∀ a b, a ⊢ a ⊕ b.
Proof.
intros a b.
realizer (λ+ λ+ λ+ [$1] $2). (* λxyz.yx *)
lam_meet. lam_leq.
Qed.
Lemma sumt_r:
∀ a b, b ⊢ a ⊕ b.
Proof.
intros a b.
realizer (λ+ λ+ λ+ [$0] $2). (* λxyz.zx *)
lam_meet. lam_leq.
Qed.
Lemma sumt_elim:
∀ a b c, a ⊢ c → b ⊢ c → a ⊕ b ⊢ c.
Proof.
intros a b c Ha Hb.
apply modus_ponens with (a0:=b↦c);auto.
apply modus_ponens with (a0:=a↦c);auto.
realizer (λ+ λ+ λ+ [[$0] $2] $1). (* λxyz.zxy *)
do 2 apply adjunction.
auto_meet_elim_trans.
Qed.
End IA.