Skip to content

Commit

Permalink
remove redundant check
Browse files Browse the repository at this point in the history
  • Loading branch information
HuStmpHrrr committed Oct 16, 2024
1 parent 9ed1a85 commit dd6e0b7
Show file tree
Hide file tree
Showing 8 changed files with 20 additions and 20 deletions.
8 changes: 4 additions & 4 deletions theories/Core/Completeness/NatCases.v
Original file line number Diff line number Diff line change
Expand Up @@ -414,8 +414,8 @@ Proof.
| _: env_relΓ ρ ?ρ0 |- _ =>
rename ρ0 into ρ'
end.
assert {{ Dom ⇑ m ≈ ⇑ m' ∈ per_nat }} by (econstructor; eassumption).
assert {{ Dom ρ ↦ ⇑ m ≈ ρ' ↦ ⇑ m' ∈ env_relΓℕ }} as HinΓℕ by (apply_relation_equivalence; mauto).
assert {{ Dom ⇑ a m ≈ ⇑ b m' ∈ per_nat }} by (econstructor; eassumption).
assert {{ Dom ρ ↦ ⇑ a m ≈ ρ' ↦ ⇑ b m' ∈ env_relΓℕ }} as HinΓℕ by (apply_relation_equivalence; mauto).
apply_relation_equivalence.
(on_all_hyp: fun H => directed destruct (H _ _ HinΓℕ)).
destruct_by_head per_univ.
Expand Down Expand Up @@ -594,8 +594,8 @@ Proof.
rename ρ1 into ρσ;
rename ρ2 into ρ'σ
end.
assert {{ Dom ⇑ m ≈ ⇑ m' ∈ per_nat }} by (econstructor; eassumption).
assert {{ Dom ρσ ↦ ⇑ m ≈ ρ'σ ↦ ⇑ m' ∈ env_relΔℕ }} as HinΔℕ by (apply_relation_equivalence; mauto).
assert {{ Dom ⇑ a m ≈ ⇑ b m' ∈ per_nat }} by (econstructor; eassumption).
assert {{ Dom ρσ ↦ ⇑ a m ≈ ρ'σ ↦ ⇑ b m' ∈ env_relΔℕ }} as HinΔℕ by (apply_relation_equivalence; mauto).
apply_relation_equivalence.
(on_all_hyp: fun H => directed destruct (H _ _ HinΔℕ)).
destruct_by_head per_univ.
Expand Down
4 changes: 2 additions & 2 deletions theories/Core/Semantic/Evaluation/Definitions.v
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,8 @@ with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
{{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ms }} )
| eval_natrec_neut :
`( {{ ⟦ MZ ⟧ ρ ↘ mz }} ->
{{ ⟦ A ⟧ ρ ↦ ⇑ m ↘ a }} ->
{{ rec ⇑ m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ⇑ a (rec m under ρ return A | zero -> mz | succ -> MS end) }} )
{{ ⟦ A ⟧ ρ ↦ ⇑ b m ↘ a }} ->
{{ rec ⇑ b m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ⇑ a (rec m under ρ return A | zero -> mz | succ -> MS end) }} )
where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' ρ '↘' r" := (eval_natrec A MZ MS m ρ r) (in custom judg)
with eval_app : domain -> domain -> domain -> Prop :=
| eval_app_fn :
Expand Down
2 changes: 1 addition & 1 deletion theories/Core/Semantic/PER/Definitions.v
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ Inductive per_nat : relation domain :=
{{ Dom succ m ≈ succ n ∈ per_nat }} }
| per_nat_neut :
`{ {{ Dom m ≈ n ∈ per_bot }} ->
{{ Dom ⇑ m ≈ ⇑ n ∈ per_nat }} }
{{ Dom ⇑ a m ≈ ⇑ b n ∈ per_nat }} }
.
#[export]
Hint Constructors per_nat : mcltt.
Expand Down
2 changes: 1 addition & 1 deletion theories/Core/Semantic/Readback/Definitions.v
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Inductive read_nf : nat -> domain_nf -> nf -> Prop :=
{{ Rnf ⇓ ℕ (succ m) in s ↘ succ M }} )
| read_nf_nat_neut :
`( {{ Rne m in s ↘ M }} ->
{{ Rnf ⇓ ℕ (⇑ m) in s ↘ ⇑ M }} )
{{ Rnf ⇓ ℕ (⇑ a m) in s ↘ ⇑ M }} )
| read_nf_fn :
`( (** Normal form of arg type *)
{{ Rtyp a in s ↘ A }} ->
Expand Down
2 changes: 1 addition & 1 deletion theories/Core/Soundness/LogicalRelation/Definitions.v
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ Inductive glu_nat : ctx -> exp -> domain -> Prop :=
| glu_nat_neut :
`{ per_bot m m ->
(forall {Δ σ M'}, {{ Δ ⊢w σ : Γ }} -> {{ Rne m in length Δ ↘ M' }} -> {{ Δ ⊢ M[σ] ≈ M' : ℕ }}) ->
glu_nat Γ M d{{{ ⇑ m }}} }.
glu_nat Γ M d{{{ ⇑ a m }}} }.

#[export]
Hint Constructors glu_nat : mcltt.
Expand Down
10 changes: 5 additions & 5 deletions theories/Core/Soundness/NatCases.v
Original file line number Diff line number Diff line change
Expand Up @@ -352,7 +352,7 @@ Qed.
#[local]
Hint Resolve cons_glu_sub_pred_q_nat_helper : mcltt.

Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M m σ ρ am P El},
Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M a m σ ρ am P El},
{{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
{{ Γ, ℕ ⊩ A : Type@i }} ->
{{ Γ ⊩ A[Id,,zero] : Type@i }} ->
Expand All @@ -362,10 +362,10 @@ Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M m σ ρ am
{{ Dom m ≈ m ∈ per_bot }} ->
(forall Δ' τ V, {{ Δ' ⊢w τ : Δ }} -> {{ Rne m in length Δ' ↘ V }} -> {{ Δ' ⊢ M[τ] ≈ V : ℕ }}) ->
{{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
{{ ⟦ A ⟧ ρ ↦ ⇑ m ↘ am }} ->
{{ ⟦ A ⟧ ρ ↦ ⇑ a m ↘ am }} ->
{{ DG am ∈ glu_univ_elem i ↘ P ↘ El }} ->
exists r,
{{ rec ⇑ m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\
{{ rec ⇑ a m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\
{{ Δ ⊢ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M] ® r ∈ El }}.
Proof.
intros * ? HA ? HMZ ? HMS **.
Expand All @@ -380,7 +380,7 @@ Proof.
invert_glu_rel_exp HA.
pose (SbΓℕA := cons_glu_sub_pred i {{{ Γ, ℕ }}} A SbΓℕ).
assert {{ EG Γ, ℕ, A ∈ glu_ctx_env ↘ SbΓℕA }} by (econstructor; mauto 3; reflexivity).
assert {{ Δ ⊢s σ,,M ® ρ ↦ ⇑ m ∈ SbΓℕ }} by (unfold SbΓℕ; mauto 3).
assert {{ Δ ⊢s σ,,M ® ρ ↦ ⇑ a m ∈ SbΓℕ }} by (unfold SbΓℕ; mauto 3).
assert {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} by mauto 2.
invert_glu_rel_exp HMS.
destruct_glu_rel_exp_with_sub.
Expand All @@ -402,7 +402,7 @@ Proof.
assert {{ ⊢ Δ, ℕ }} by mauto 3.
assert {{ Δ, ℕ ⊢ A[q σ] : Type@i }} by mauto 3.
assert {{ ⊢ Δ, ℕ, A[q σ] }} by mauto 2.
assert {{ Δ ⊢ M : ℕ }} by mauto 3.
unshelve assert {{ Δ ⊢ M : ℕ }} by mauto 3; [constructor |].
assert {{ Δ ⊢ ℕ : Type@0 }} by mauto 3.
assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} by mauto 3.
assert {{ Δ ⊢ M : ℕ[σ] }} by mauto 3.
Expand Down
8 changes: 4 additions & 4 deletions theories/Extraction/Evaluation.v
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,8 @@ with eval_natrec_order : exp -> exp -> exp -> domain -> env -> Prop :=
eval_natrec_order A MZ MS d{{{ succ b }}} p )
| eno_neut :
`( eval_exp_order MZ p ->
eval_exp_order A d{{{ p ↦ ⇑ m }}} ->
eval_natrec_order A MZ MS d{{{ ⇑ m }}} p )
eval_exp_order A d{{{ p ↦ ⇑ a m }}} ->
eval_natrec_order A MZ MS d{{{ ⇑ a m }}} p )

with eval_app_order : domain -> domain -> Prop :=
| eao_fn :
Expand Down Expand Up @@ -146,9 +146,9 @@ with eval_natrec_impl A MZ MS m p (H : eval_natrec_order A MZ MS m p) : { d | ev
let (mr, Hmr) := eval_natrec_impl A MZ MS m p _ in
let (r, Hr) := eval_exp_impl MS d{{{ p ↦ m ↦ mr }}} _ in
exist _ r _
| A, MZ, MS, d{{{ ⇑ m }}} , p, H =>
| A, MZ, MS, d{{{ ⇑ a m }}} , p, H =>
let (mz, Hmz) := eval_exp_impl MZ p _ in
let (mA, HmA) := eval_exp_impl A d{{{ p ↦ ⇑ m }}} _ in
let (mA, HmA) := eval_exp_impl A d{{{ p ↦ ⇑ a m }}} _ in
exist _ d{{{ ⇑ mA (rec m under p return A | zero -> mz | succ -> MS end) }}} _

with eval_app_impl m n (H : eval_app_order m n) : { d | eval_app m n d } by struct H :=
Expand Down
4 changes: 2 additions & 2 deletions theories/Extraction/Readback.v
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ Inductive read_nf_order : nat -> domain_nf -> Prop :=
read_nf_order s d{{{ ⇓ ℕ (succ m) }}} )
| rnf_nat_neut :
`( read_ne_order s m ->
read_nf_order s d{{{ ⇓ ℕ (⇑ m) }}} )
read_nf_order s d{{{ ⇓ ℕ (⇑ a m) }}} )
| rnf_fn :
`( read_typ_order s a ->
eval_app_order m d{{{ ⇑! a s }}} ->
Expand Down Expand Up @@ -119,7 +119,7 @@ Equations read_nf_impl s d (H : read_nf_order s d) : { m | {{ Rnf d in s ↘ m }
| s, d{{{ ⇓ ℕ (succ m) }}} , H =>
let (M, HM) := read_nf_impl s d{{{ ⇓ ℕ m }}} _ in
exist _ n{{{ succ M }}} _
| s, d{{{ ⇓ ℕ (⇑ m) }}} , H =>
| s, d{{{ ⇓ ℕ (⇑ ^_ m) }}} , H =>
let (M, HM) := read_ne_impl s m _ in
exist _ n{{{ ⇑ M }}} _
| s, d{{{ ⇓ (Π a p B) m }}}, H =>
Expand Down

0 comments on commit dd6e0b7

Please sign in to comment.