Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change isomorphism between per_elem #81

Merged
merged 10 commits into from
May 17, 2024
Merged

Change isomorphism between per_elem #81

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
f461cb2
[WIP] Change isomorphism between per_elem
Ailrun May 15, 2024
a1cbd61
Change minor thing
Ailrun May 15, 2024
3e8f170
Finish change of basic lemmas
Ailrun May 16, 2024
e1d97ff
Restore Realizability
Ailrun May 16, 2024
7690e18
Improve proofs
Ailrun May 17, 2024
f733215
Restore all proofs
Ailrun May 17, 2024
73754e1
Fix missing one as well
Ailrun May 17, 2024
1054596
Fix some proofs
Ailrun May 17, 2024
542529f
Add a pi case
Ailrun May 17, 2024
476efa9
Add one more case
Ailrun May 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
99 changes: 58 additions & 41 deletions theories/Core/Semantic/PER/Definitions.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,56 +83,66 @@ Section Per_univ_elem_core_def.

Inductive per_univ_elem_core : relation domain -> domain -> domain -> Prop :=
| per_univ_elem_core_univ :
`{ forall (lt_j_i : j < i),
`{ forall (elem_rel : relation domain)
(lt_j_i : j < i),
j = j' ->
{{ DF 𝕌@j ≈ 𝕌@j' ∈ per_univ_elem_core ↘ per_univ_rec lt_j_i }} }
| per_univ_elem_core_nat : {{ DF ℕ ≈ ℕ ∈ per_univ_elem_core ↘ per_nat }}
(forall a a', elem_rel a a' <-> per_univ_rec lt_j_i a a') ->
{{ DF 𝕌@j ≈ 𝕌@j' ∈ per_univ_elem_core ↘ elem_rel }} }
| per_univ_elem_core_nat :
forall (elem_rel : relation domain),
(forall m m', elem_rel m m' <-> per_nat m m') ->
{{ DF ℕ ≈ ℕ ∈ per_univ_elem_core ↘ elem_rel }}
| per_univ_elem_core_pi :
`{ forall (in_rel : relation domain)
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
(elem_rel : relation domain)
(equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel}}),
PER in_rel ->
(forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
rel_mod_eval per_univ_elem_core B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
(forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
(forall f f', elem_rel f f' <-> forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
{{ DF Π a p B ≈ Π a' p' B' ∈ per_univ_elem_core ↘ elem_rel }} }
| per_univ_elem_core_neut :
`{ {{ Dom b ≈ b' ∈ per_bot }} ->
{{ DF ⇑ a b ≈ ⇑ a' b' ∈ per_univ_elem_core ↘ per_ne }} }
`{ forall (elem_rel : relation domain),
{{ Dom b ≈ b' ∈ per_bot }} ->
(forall m m', elem_rel m m' <-> per_ne m m') ->
{{ DF ⇑ a b ≈ ⇑ a' b' ∈ per_univ_elem_core ↘ elem_rel }} }
.

Hypothesis
(motive : relation domain -> domain -> domain -> Prop)
(case_U : forall (j j' : nat) (lt_j_i : j < i), j = j' -> motive (per_univ_rec lt_j_i) d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}})
(case_nat : motive per_nat d{{{ ℕ }}} d{{{ ℕ }}})
(case_U : forall {j j' elem_rel} (lt_j_i : j < i), j = j' -> (forall a a', elem_rel a a' <-> per_univ_rec lt_j_i a a') -> motive elem_rel d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}})
(case_nat : forall {elem_rel}, (forall m m', elem_rel m m' <-> per_nat m m') -> motive elem_rel d{{{ ℕ }}} d{{{ ℕ }}})
(case_Pi :
forall {A p B A' p' B' in_rel elem_rel}
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
forall {A p B A' p' B' in_rel}
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
{elem_rel},
{{ DF A ≈ A' ∈ per_univ_elem_core ↘ in_rel }} ->
motive in_rel A A' ->
PER in_rel ->
(forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
rel_mod_eval (fun R x y => {{ DF x ≈ y ∈ per_univ_elem_core ↘ R }} /\ motive R x y) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
(forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
(forall f f', elem_rel f f' <-> forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
motive elem_rel d{{{ Π A p B }}} d{{{ Π A' p' B' }}})
(case_ne : (forall {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive per_ne d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}})).
(case_ne : (forall {a b a' b' elem_rel}, {{ Dom b ≈ b' ∈ per_bot }} -> (forall m m', elem_rel m m' <-> per_ne m m') -> motive elem_rel d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}})).

#[derive(equations=no, eliminator=no)]
Equations per_univ_elem_core_strong_ind R a b (H : {{ DF a ≈ b ∈ per_univ_elem_core ↘ R }}) : {{ DF a ≈ b ∈ motive ↘ R }} :=
| R, a, b, (per_univ_elem_core_univ lt_j_i eq) => case_U _ _ lt_j_i eq;
| R, a, b, per_univ_elem_core_nat => case_nat;
| R, a, b, (per_univ_elem_core_pi in_rel out_rel equiv_a_a' per HT HE) =>
| R, a, b, (per_univ_elem_core_univ _ lt_j_i HE eq) => case_U lt_j_i HE eq;
| R, a, b, (per_univ_elem_core_nat _ HE) => case_nat HE;
| R, a, b, (per_univ_elem_core_pi _ out_rel _ equiv_a_a' per HT HE) =>
case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a') per
(fun _ _ equiv_c_c' => match HT _ _ equiv_c_c' with
| mk_rel_mod_eval b b' evb evb' Rel =>
mk_rel_mod_eval b b' evb evb' (conj _ (per_univ_elem_core_strong_ind _ _ _ Rel))
end)
HE;
| R, a, b, (per_univ_elem_core_neut equiv_b_b') => case_ne equiv_b_b'.
| R, a, b, (per_univ_elem_core_neut _ equiv_b_b' HE) => case_ne equiv_b_b' HE.

End Per_univ_elem_core_def.

Global Hint Constructors per_univ_elem_core : mcltt.
#[export]
Hint Constructors per_univ_elem_core : mcltt.

Equations per_univ_elem (i : nat) : relation domain -> domain -> domain -> Prop by wf i :=
| i => per_univ_elem_core i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}).
Expand All @@ -141,38 +151,44 @@ Definition per_univ (i : nat) : relation domain := fun a a' => exists R', {{ DF
#[global]
Arguments per_univ _ _ _ /.

Lemma per_univ_elem_core_univ' : forall j i,
Lemma per_univ_elem_core_univ' : forall j i elem_rel,
j < i ->
{{ DF 𝕌@j ≈ 𝕌@j ∈ per_univ_elem i ↘ per_univ j }}.
(forall a a', elem_rel a a' <-> per_univ j a a') ->
{{ DF 𝕌@j ≈ 𝕌@j ∈ per_univ_elem i ↘ elem_rel }}.
Proof.
intros.
simp per_univ_elem.

eapply (per_univ_elem_core_univ i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}) H).
apply per_univ_elem_core_univ; try assumption.
reflexivity.
Qed.
Global Hint Resolve per_univ_elem_core_univ' : mcltt.
#[export]
Hint Resolve per_univ_elem_core_univ' : mcltt.

(** Universe/Element PER Induction Principle *)

Section Per_univ_elem_ind_def.
Hypothesis
(motive : nat -> relation domain -> domain -> domain -> Prop)
(case_U : forall j j' i, j < i -> j = j' ->
(forall A B R, {{ DF A ≈ B ∈ per_univ_elem j ↘ R }} -> motive j R A B) ->
motive i (per_univ j) d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}})
(case_N : forall i, motive i per_nat d{{{ ℕ }}} d{{{ ℕ }}})
(case_U : forall i {j j' elem_rel},
j < i -> j = j' ->
(forall a a', elem_rel a a' <-> per_univ j a a') ->
(forall A B R, {{ DF A ≈ B ∈ per_univ_elem j ↘ R }} -> motive j R A B) ->
motive i elem_rel d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}})
(case_N : forall i {elem_rel},
(forall m m', elem_rel m m' <-> per_nat m m') ->
motive i elem_rel d{{{ ℕ }}} d{{{ ℕ }}})
(case_Pi :
forall i {A p B A' p' B' in_rel elem_rel}
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
forall i {A p B A' p' B' in_rel}
(out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
{elem_rel},
{{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel }} ->
motive i in_rel A A' ->
PER in_rel ->
(forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
rel_mod_eval (fun R x y => {{ DF x ≈ y ∈ per_univ_elem i ↘ R }} /\ motive i R x y) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
(forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
(forall f f', elem_rel f f' <-> forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
motive i elem_rel d{{{ Π A p B }}} d{{{ Π A' p' B' }}})
(case_ne : (forall i {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive i per_ne d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}})).
(case_ne : (forall i {a b a' b' elem_rel}, {{ Dom b ≈ b' ∈ per_bot }} -> (forall m m', elem_rel m m' <-> per_ne m m') -> motive i elem_rel d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}})).

#[local]
Ltac def_simp := simp per_univ_elem in *.
Expand All @@ -182,16 +198,15 @@ Section Per_univ_elem_ind_def.
(H : {{ DF a ≈ b ∈ per_univ_elem_core i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}) ↘ R }}) : {{ DF a ≈ b ∈ motive i ↘ R }} by wf i :=
| i, R, a, b, H =>
per_univ_elem_core_strong_ind i _ (motive i)
(fun j j' j_lt_i eq => case_U j j' i j_lt_i eq (fun A B R' H' => per_univ_elem_ind' _ R' A B _))
(case_N i)
(fun A p B A' p' B' in_rel elem_rel out_rel HA IHA per HT HE => case_Pi i out_rel _ IHA per _ HE)
(@case_ne i)
(fun _ _ _ j_lt_i eq HE => case_U i j_lt_i eq HE (fun A B R' H' => per_univ_elem_ind' _ R' A B _))
(fun _ => case_N i)
(fun _ _ _ _ _ _ _ out_rel _ _ IHA per _ => case_Pi i out_rel _ IHA per _)
(fun _ _ _ _ _ => case_ne i)
R a b H.

#[derive(equations=no, eliminator=no), tactic="def_simp"]
Equations per_univ_elem_ind i a b R (H : per_univ_elem i a b R) : motive i a b R :=
| i, a, b, R, H := per_univ_elem_ind' i a b R _.

End Per_univ_elem_ind_def.

(** Universe/Element PER Helper Tactics *)
Expand All @@ -212,20 +227,22 @@ Ltac per_univ_elem_econstructor :=
Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
Arguments rel_typ _ _ _ _ _ _ /.

Definition per_total : relation env := fun p p' => True.

Inductive per_ctx_env : relation env -> ctx -> ctx -> Prop :=
| per_ctx_env_nil :
`{ {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ per_total }} }
`{ forall env_rel,
(forall p p', env_rel p p' <-> True) ->
{{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ env_rel }} }
| per_ctx_env_cons :
`{ forall (tail_rel : relation env)
`{ forall tail_rel
(head_rel : forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), relation domain)
env_rel
(equiv_Γ_Γ' : {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ tail_rel }}),
PER tail_rel ->
(forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}),
rel_typ i A p A' p' (head_rel equiv_p_p')) ->
(env_rel = fun p p' => exists (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ tail_rel }}),
{{ Dom ~(p 0) ≈ ~(p' 0) ∈ head_rel equiv_p_drop_p'_drop }}) ->
(forall p p', env_rel p p' <->
exists (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ tail_rel }}),
{{ Dom ~(p 0) ≈ ~(p' 0) ∈ head_rel equiv_p_drop_p'_drop }}) ->
{{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ env_rel }} }
.

Expand Down
Loading
Loading