Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add simple induction principle
Browse files Browse the repository at this point in the history
Ailrun committed Jan 22, 2024
1 parent 6006b74 commit a629131
Showing 1 changed file with 28 additions and 0 deletions.
28 changes: 28 additions & 0 deletions theories/Core/Semantic/PERLemmas.v
Original file line number Diff line number Diff line change
@@ -72,3 +72,31 @@ Proof with solve [mauto].
Unshelve.
all: assumption.
Qed.

Lemma per_univ_ind : forall i P,
(forall j j', j < i -> j = j' -> {{ Dom 𝕌@j ≈ 𝕌@j' ∈ P }}) ->
{{ Dom ℕ ≈ ℕ ∈ P }} ->
(forall a a' B p B' p'
(equiv_a_a' : {{ Dom a ≈ a' ∈ per_univ i }}),
{{ Dom a ≈ a' ∈ P }} ->
(forall c c',
{{ Dom c ≈ c' ∈ per_elem equiv_a_a' }} ->
rel_mod_eval (per_univ i) B d{{{ p ↦ c}}} B' d{{{ p' ↦ c'}}}) ->
{{ Dom Π a p B ≈ Π a' p' B' ∈ P }}) ->
(forall m m' a a', {{ Dom m ≈ m' ∈ per_bot }} -> {{ Dom ⇑ a m ≈ ⇑ a' m' ∈ P }}) ->
forall d d', {{ Dom d ≈ d' ∈ per_univ i }} -> {{ Dom d ≈ d' ∈ P }}.
Proof with solve [mauto].
intros * Huniv Hnat Hpi Hneut d d' [equiv_d_d'_template equiv_d_d'_check].
induction equiv_d_d'_check; only 1-2,4: solve [mauto].
unshelve epose (equiv_a_a'_real := _ : {{ Dom a ≈ a' ∈ per_univ i }}).
{ econstructor... }
eapply Hpi with (equiv_a_a' := equiv_a_a'_real); subst equiv_a_a'_real; [solve [mauto]|].
intros * equiv_c_c'.
unfold per_elem, Per_univ_def.per_elem in equiv_c_c'.
destruct (rel_B_B' _ _ equiv_c_c').
econstructor; only 1-2: solve [mauto].
intros b b' eval_B eval_B'.
econstructor; apply H.
Unshelve.
3-5: eassumption.
Qed.

0 comments on commit a629131

Please sign in to comment.