Skip to content

cleanup in FinNat #2138

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

Merged
Alizter merged 14 commits into from
Nov 17, 2024
Merged

cleanup in FinNat #2138

Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
d360028
reduce universes in FinNat
Alizter Nov 14, 2024
9a2f679
FinNat: rm path_{zero,last}_finnat; adapt path_succ_finnat; simplify …
jdchristensen Nov 16, 2024
8a8c623
FinNat: get rid of one more universe variable
jdchristensen Nov 16, 2024
2a7d9da
FinNat: remove Monomorphic keyword
jdchristensen Nov 16, 2024
3ef6845
refine imports in FinNat.v
Alizter Nov 15, 2024
877a200
improve proof of path_finnat_to_fin_incl
Alizter Nov 15, 2024
ee4e953
improve lt_fin_to_nat
Alizter Nov 15, 2024
2bbce36
remove unused and unnecessary lemmas
Alizter Nov 17, 2024
b170a3a
change Lemma to Definition and enforce uni vars
Alizter Nov 17, 2024
bee8032
rename compute_* lemmas to *_beta* lemmas
Alizter Nov 17, 2024
309dbf2
fix universe issue in 8.19
Alizter Nov 17, 2024
7d7e143
revert removal of path_succ_finnat
Alizter Nov 17, 2024
cdeb723
revert to other version of path_succ_finnat
Alizter Nov 17, 2024
7567113
trim whitespace
Alizter Nov 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
10 changes: 8 additions & 2 deletions theories/Spaces/Finite/FinNat.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,12 @@ Definition zero_finnat@{} (n : nat) : FinNat n.+1

Definition succ_finnat@{} {n : nat} (u : FinNat n) : FinNat n.+1
:= (u.1.+1; leq_succ u.2).

Definition path_succ_finnat@{} {n : nat} (u : FinNat n) (h : u.1.+1 < n.+1)
: succ_finnat u = (u.1.+1; h).
Proof.
by apply path_sigma_hprop.
Defined.

Definition last_finnat@{} (n : nat) : FinNat n.+1
:= exist (fun x => x < n.+1) n (leq_refl n.+1).
Expand All @@ -34,8 +40,8 @@ Proof.
destruct x as [| x].
+ nrefine (transport (P n.+1) _ (z _)).
by apply path_sigma_hprop.
+ refine (transport (P n.+1) _ (s _ _ (IHn (x; leq_pred' _)))).
by apply path_sigma_hprop.
+ refine (transport (P n.+1) (path_succ_finnat (x; leq_pred' h) _) _).
apply s. apply IHn.
Defined.

Definition finnat_ind_beta_zero@{u} (P : forall n : nat, FinNat n -> Type@{u})
Expand Down
Loading