Require Import stdpp.base.
Require Import stdpp.decidable.
Require Import stdpp.countable.
Require Import skylabs.prelude.base.
Require Import skylabs.prelude.option.
Require Import skylabs.prelude.list_numbers.
Require Import skylabs.prelude.finite.
#[local] Open Scope N_scope.
Implicit Types (n : N) (p : positive).
Module Import TO_UPSTREAM_TRANSPARENT.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
Lemma f_equal_help {A B} (f g : A → B) x y : f = g → x = y → f x = g y.
Section dsig_transparent.
Context {A : Type} {P : A → Prop} `{!∀ x, Decision (P x)}.
Lemma dsig_eq_pi (x y : dsig P) : `x = `y ↔ x = y.
#[global] Instance dsig_eq_dec `{!EqDecision A} : EqDecision (dsig P).
#[global] Program Instance countable_dsig `{Countable A} :
Countable (dsig P) :=
inj_countable proj1_sig (λ x, Hx ← guard (bool_decide (P x)); Some (x ↾ Hx)) _.
End dsig_transparent.
End TO_UPSTREAM_TRANSPARENT.
Module fin.
Definition t n : Set := {m : N | bool_decide (m < n)}.
Definition mk (m : N) {n : N} (prf : m < n) : fin.t n :=
m ↾ bool_decide_pack _ prf.
#[global] Arguments mk m & {n} prf.
The lit m notation works if both m and the bound n are ground,
since then eq_refl is a valid proof of m < n.
Notation lit m := (mk m eq_refl).
Lemma t_0_inv : fin.t 0 → False.
Lemma t_inv {n} (i : fin.t n) : 0 < n.
Lemma t_0_inv : fin.t 0 → False.
Lemma t_inv {n} (i : fin.t n) : 0 < n.
Definition of_N' {n : N} (Hn : 0 < n) (m : N) : fin.t n :=
match decide (m < n)%N with
| left prf ⇒ mk m prf
| right _ ⇒ mk 0 Hn
end.
Definition of_nat' {n : N} (Hn : 0 < n) (m : nat) : fin.t n :=
of_N' Hn (N.of_nat m).
Definition of_N (p : positive) (m : N) : t (Npos p) :=
of_N' (n := Npos p) eq_refl m.
Definition of_nat (p : positive) (m : nat) : fin.t (Npos p) :=
fin.of_N p (N.of_nat m).
Definition to_N {n} (f : t n) : N := `f.
Lemma to_N_lt {n} (f : t n) : to_N f < n.
Definition t_eq {n} (x1 x2 : t n)
(Heq : to_N x1 = to_N x2) : x1 = x2.
Lemma to_of_N' {n} (Hn : 0 < n) (m : N) : m < n → to_N (of_N' Hn m) = m.
Lemma to_of_N_gt' {n} (Hn : 0 < n) (m : N) : n ≤ m → to_N (of_N' Hn m) = 0.
Lemma of_to_N' {n} (Hn : 0 < n) (x : t n) : of_N' Hn (to_N x) = x.
Lemma to_of_N (p : positive) (m : N) : m < N.pos p → to_N (of_N p m) = m.
Lemma proj_sig1_of_N (p : positive) (m : N) : m < N.pos p → proj1_sig (of_N p m) = m.
Lemma of_to_N {p} (x : t (N.pos p)) : of_N p (to_N x) = x.
Lemma to_of_N_gt (p : positive) (m : N) : N.pos p ≤ m → to_N (of_N p m) = 0.
Lemma proj1_sig_of_N p (m : N) : m < N.pos p → proj1_sig (of_N p m) = m.
match decide (m < n)%N with
| left prf ⇒ mk m prf
| right _ ⇒ mk 0 Hn
end.
Definition of_nat' {n : N} (Hn : 0 < n) (m : nat) : fin.t n :=
of_N' Hn (N.of_nat m).
Definition of_N (p : positive) (m : N) : t (Npos p) :=
of_N' (n := Npos p) eq_refl m.
Definition of_nat (p : positive) (m : nat) : fin.t (Npos p) :=
fin.of_N p (N.of_nat m).
Definition to_N {n} (f : t n) : N := `f.
Lemma to_N_lt {n} (f : t n) : to_N f < n.
Definition t_eq {n} (x1 x2 : t n)
(Heq : to_N x1 = to_N x2) : x1 = x2.
Lemma to_of_N' {n} (Hn : 0 < n) (m : N) : m < n → to_N (of_N' Hn m) = m.
Lemma to_of_N_gt' {n} (Hn : 0 < n) (m : N) : n ≤ m → to_N (of_N' Hn m) = 0.
Lemma of_to_N' {n} (Hn : 0 < n) (x : t n) : of_N' Hn (to_N x) = x.
Lemma to_of_N (p : positive) (m : N) : m < N.pos p → to_N (of_N p m) = m.
Lemma proj_sig1_of_N (p : positive) (m : N) : m < N.pos p → proj1_sig (of_N p m) = m.
Lemma of_to_N {p} (x : t (N.pos p)) : of_N p (to_N x) = x.
Lemma to_of_N_gt (p : positive) (m : N) : N.pos p ≤ m → to_N (of_N p m) = 0.
Lemma proj1_sig_of_N p (m : N) : m < N.pos p → proj1_sig (of_N p m) = m.
Declared an instance, because it is not redudant after t is made opaque.
#[global] Instance to_N_inj n : Inj eq eq (to_N (n := n)) := _.
#[global] Instance t_eq_dec n : EqDecision (t n) := _.
#[global] Instance t_countable n : Countable (t n) := _.
#[global] Instance t_pos_inhabited p : Inhabited (t (Npos p)).
Lemma t_gt_inhabited n (Hn : 0 < n) : Inhabited (t n).
#[global] Hint Opaque t : typeclass_instances.
#[global] Instance t_eq_dec n : EqDecision (t n) := _.
#[global] Instance t_countable n : Countable (t n) := _.
#[global] Instance t_pos_inhabited p : Inhabited (t (Npos p)).
Lemma t_gt_inhabited n (Hn : 0 < n) : Inhabited (t n).
#[global] Hint Opaque t : typeclass_instances.
#[program] Definition weaken' {m n} (x : fin.t m) (prf : m ≤ n) : fin.t n :=
fin.mk (fin.to_N x) _.
#[global] Arguments weaken' {m} & {n} x prf.
fin.mk (fin.to_N x) _.
#[global] Arguments weaken' {m} & {n} x prf.
weaken_bool_decide is equivalent to weaken'.
But instead of (m ≤ n) we take bool_decide (m ≤ n) = true, because
that is provable by eq_refl when m and n are ground.
#[program] Definition weaken_bool_decide {m n} (x : fin.t m)
(prf : bool_decide (m ≤ n) = true) : fin.t n :=
weaken' x _.
#[global] Arguments weaken_bool_decide {m} & {n} x prf.
(prf : bool_decide (m ≤ n) = true) : fin.t n :=
weaken' x _.
#[global] Arguments weaken_bool_decide {m} & {n} x prf.
The weaken x notation converts x : fin.t m to fin.t n.
This assumes both m and n are ground, so that then eq_refl is a valid
argument for prf.
Notation weaken x := (weaken_bool_decide x eq_refl).
Goal (weaken (lit 10 : fin.t 11) : fin.t 42) = (lit 10 : fin.t 42).
Goal (weaken (lit 10 : fin.t 11) : fin.t 11) = (lit 10 : fin.t 11).
Definition seq (n : N) : list (t n) :=
match n with
| N0 ⇒ []
| Npos max ⇒ fin.of_N max <$> seqN 0 (Npos max)
end.
Lemma seq_lenN n : lengthN (seq n) = n.
Lemma seq_len n : length (seq n) = N.to_nat n.
Lemma seq_NoDup n : NoDup (seq n).
Lemma elem_of_seq n {i : t n} : i ∈ seq n.
Lemma seq_lookupN n t : fin.seq n !! fin.to_N t = Some t.
#[global, refine] Instance t_finite n : Finite (t n) :=
{ enum := seq n; }.
Lemma enum_unfold n : enum (fin.t n) = fin.seq n.
Goal (weaken (lit 10 : fin.t 11) : fin.t 42) = (lit 10 : fin.t 42).
Goal (weaken (lit 10 : fin.t 11) : fin.t 11) = (lit 10 : fin.t 11).
Definition seq (n : N) : list (t n) :=
match n with
| N0 ⇒ []
| Npos max ⇒ fin.of_N max <$> seqN 0 (Npos max)
end.
Lemma seq_lenN n : lengthN (seq n) = n.
Lemma seq_len n : length (seq n) = N.to_nat n.
Lemma seq_NoDup n : NoDup (seq n).
Lemma elem_of_seq n {i : t n} : i ∈ seq n.
Lemma seq_lookupN n t : fin.seq n !! fin.to_N t = Some t.
#[global, refine] Instance t_finite n : Finite (t n) :=
{ enum := seq n; }.
Lemma enum_unfold n : enum (fin.t n) = fin.seq n.
Conversion to and from the "indexed fin" type fin from the stdlib.
#[program] Definition to_idx_fin' {m : N} (f : fin.t m) {n : nat} (_ : m = N.of_nat n) : fin n :=
nat_to_fin (p := N.to_nat (fin.to_N f)) _.
#[global] Arguments to_idx_fin' {m} f & {n} prf. Notation to_idx_fin x := (to_idx_fin' x eq_refl).
#[program] Definition of_idx_fin' {m : nat} (f : fin m) {n : N} (_ : n = N.of_nat m) : fin.t n :=
fin.mk (N.of_nat (fin_to_nat f)) _.
#[global] Arguments of_idx_fin' {m} f & {n} prf. Notation of_idx_fin x := (of_idx_fin' x eq_refl).
Lemma of_to_idx_fin_cancel {m : N} {n : nat} (f : fin.t m) (E : m = N.of_nat n) :
of_idx_fin' (to_idx_fin' f E) E = f.
Lemma to_of_idx_fin_cancel {m : N} {n : nat} (f : fin n) (E : m = N.of_nat n) :
to_idx_fin' (of_idx_fin' f E) E = f.
Definition decode `{Finite A} (f : fin.t (N.of_nat (card A))) : A :=
decode_fin (to_idx_fin f).
#[global] Arguments decode & {A _ _} f.
nat_to_fin (p := N.to_nat (fin.to_N f)) _.
#[global] Arguments to_idx_fin' {m} f & {n} prf. Notation to_idx_fin x := (to_idx_fin' x eq_refl).
#[program] Definition of_idx_fin' {m : nat} (f : fin m) {n : N} (_ : n = N.of_nat m) : fin.t n :=
fin.mk (N.of_nat (fin_to_nat f)) _.
#[global] Arguments of_idx_fin' {m} f & {n} prf. Notation of_idx_fin x := (of_idx_fin' x eq_refl).
Lemma of_to_idx_fin_cancel {m : N} {n : nat} (f : fin.t m) (E : m = N.of_nat n) :
of_idx_fin' (to_idx_fin' f E) E = f.
Lemma to_of_idx_fin_cancel {m : N} {n : nat} (f : fin n) (E : m = N.of_nat n) :
to_idx_fin' (of_idx_fin' f E) E = f.
Definition decode `{Finite A} (f : fin.t (N.of_nat (card A))) : A :=
decode_fin (to_idx_fin f).
#[global] Arguments decode & {A _ _} f.
Eta-rule for fin.mk.
Prove the natural elimination principle you would get from a sigma type.
However, to prove ∀ x ; fin.t n, ..., it's much simpler to use
move=> x /bool_decide_unpack.
>>
Qed because reduction gets stuck, and this seems hard to fix.
Lemma t_sig_rect (P : ∀ n, fin.t n → Type)
(Hp : ∀ n m (H : m < n), P n (fin.mk m H)) :
∀ n (x : fin.t n), P n x.
(Hp : ∀ n m (H : m < n), P n (fin.mk m H)) :
∀ n (x : fin.t n), P n x.
Eta-rule for zero
"Smart constructor" fin.succ
Eta-rule for fin.succ
Lemma is_succ {x n} {Hl : bool_decide (N.succ x < N.succ n)} :
N.succ x ↾ Hl = fin.succ (fin.mk x (proj1 (N_succ_lt_mono_inv _ _) (bool_decide_unpack _ Hl))).
N.succ x ↾ Hl = fin.succ (fin.mk x (proj1 (N_succ_lt_mono_inv _ _) (bool_decide_unpack _ Hl))).
Peano-like elimination principle.
Qed because reduction gets stuck, and this seems hard to fix.
Lemma t_rect (P : ∀ n, fin.t n → Type)
(Hz : ∀ n, P (N.succ n) fin.zero)
(Hs : ∀ n (x : fin.t n), P (N.succ n) (fin.succ x)) :
∀ n (x : fin.t n), P n x.
End fin.
Module Type Test.
Fact test1 : @fin.mk 0 1 eq_refl = 0 ↾ I.
Fact test2 : decide (@fin.mk 0 1 eq_refl = @fin.mk 0 1 eq_refl) = left eq_refl.
End Test.
(Hz : ∀ n, P (N.succ n) fin.zero)
(Hs : ∀ n (x : fin.t n), P (N.succ n) (fin.succ x)) :
∀ n (x : fin.t n), P n x.
End fin.
Module Type Test.
Fact test1 : @fin.mk 0 1 eq_refl = 0 ↾ I.
Fact test2 : decide (@fin.mk 0 1 eq_refl = @fin.mk 0 1 eq_refl) = left eq_refl.
End Test.
This page has been generated by coqdoc