Skip to content

Commit

Permalink
[WIP] Change isomorphism between per_elem
Browse files Browse the repository at this point in the history
  • Loading branch information
@Ailrun
Ailrun committed May 15, 2024
1 parent 023acf2 commit f461cb2
Show file tree
Hide file tree
Showing 2 changed files with 217 additions and 137 deletions.
97 changes: 57 additions & 40 deletions theories/Core/Semantic/PER/Definitions.v
View file
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)
(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 _ HA IHA per HT HE => case_Pi i out_rel _ IHA per _ HE)
(@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

0 comments on commit f461cb2

Please sign in to comment.