Timings for SuccessorStructure.v
Require Import Spaces.Int.Core.
Require Import Spaces.Finite.Fin.
Require Import WildCat.Core.
Local Set Universe Minimization ToSet.
(** * Successor Structures. *)
(** A successor structure is just a type with a endofunctor on it, called 'successor'. Typical examples include either the integers or natural numbers with the successor (or predecessor) operation. *)
Record SuccStr : Type := {
ss_carrier :> Type ;
ss_succ : ss_carrier -> ss_carrier ;
}.
Declare Scope succ_scope.
Local Open Scope nat_scope.
Local Open Scope type_scope.
Local Open Scope succ_scope.
Delimit Scope succ_scope with succ.
Notation "x .+1" := (ss_succ x) : succ_scope.
(** Successor structure of naturals *)
Definition NatSucc : SuccStr := Build_SuccStr nat Nat.Core.succ.
(** Successor structure of integers *)
Definition IntSucc : SuccStr := Build_SuccStr Int int_succ.
Notation "'+N'" := NatSucc : succ_scope.
Notation "'+Z'" := IntSucc : succ_scope.
(** Stratified successor structures *)
(** If [N] has a successor structure, then so does the product [N * Fin n]. The successor operation increases the second factor, and if it wraps around, it also increases the first factor. *)
Definition StratifiedType (N : SuccStr) (n : nat) := N * Fin n.
Definition stratified_succ (N : SuccStr) (n : nat) (x : StratifiedType N n)
: StratifiedType N n.
exact (Empty_rec _ (snd x)).
destruct (dec (snd x = inr tt)).
exact (fsucc_mod (snd x)).
Definition Stratified (N : SuccStr) (n : nat) : SuccStr
:= Build_SuccStr (StratifiedType N n) (stratified_succ N n).
(** Addition in successor structures *)
Definition ss_add {N : SuccStr} (n : N) (k : nat) : N := nat_iter k ss_succ n.
Infix "+" := ss_add : succ_scope.
Definition ss_add_succ {N : SuccStr} (n : N) (k : nat)
: n + k.+1 = n.+1 + k
:= nat_iter_succ_r k ss_succ n.
Definition ss_add_sum {N : SuccStr} (n : N) (k l : nat)
: n + (k + l) = (n + l) + k
:= nat_iter_add k l ss_succ n.
(** Nat and Int segmented by triples *)
Notation "'N3'" := (Stratified (+N) 3) : succ_scope.
Notation "'Z3'" := (Stratified (+Z) 3) : succ_scope.
(** ** Category of successor structures *)
(** Inspired by the construction of the wildcat structure on pType, we can give SuccStr a wildcat structure in a similar manner (all the way up). *)
Record ssFam (A : SuccStr) := {
ss_fam :> A -> Type;
dss_succ {x} : ss_fam x -> ss_fam (x.+1);
}.
Arguments ss_fam {_ _} _.
Arguments dss_succ {_ _ _}.
Record ssForall {A : SuccStr} (B : ssFam A) := {
ss_fun :> forall x, B x;
ss_fun_succ : forall x, ss_fun x.+1 = dss_succ (ss_fun x);
}.
Arguments ss_fun {_ _} _ _.
Arguments ss_fun_succ {_ _} _ _.
Definition ssfam_const {A : SuccStr} (B : SuccStr) : ssFam A
:= Build_ssFam A (fun _ => B) (fun _ => ss_succ).
Definition ssfam_sshomotopy {A : SuccStr} {P : ssFam A} (f g : ssForall P)
: ssFam A.
1: exact (fun x => f x = g x).
refine (ss_fun_succ f x @ ap dss_succ p @ (ss_fun_succ g x)^).
Definition ssHomotopy {A : SuccStr} {P : ssFam A} (f g : ssForall P)
:= ssForall (ssfam_sshomotopy f g).
Global Instance isgraph_ss : IsGraph SuccStr.
exact (@ssForall X (ssfam_const Y)).
Global Instance isgraph_ssforall {A : SuccStr} (P : ssFam A)
: IsGraph (ssForall P).
Global Instance is2graph_ssforall {A : SuccStr} (P : ssFam A)
: Is2Graph (ssForall P)
:= {}.
Global Instance is2graph_ss : Is2Graph SuccStr := {}.
Global Instance is3graph_ss : Is3Graph SuccStr := {}.
Ltac sselim_elim eq x :=
match type of (eq x) with
| ?lhs = _ =>
generalize dependent (eq x);
generalize dependent lhs
| _ => fail "sselim: no lhs found"
end.
Ltac sselim f :=
let eq := fresh "eq" in
destruct f as [f eq];
cbn in *;
match type of eq with
| forall x : ?X, _ = _ =>
multimatch goal with
| x : X |- _ => sselim_elim eq x
| f : ?Y -> X |- _ =>
match goal with
| y : Y |- _ => sselim_elim eq (f y)
| g : ?Z -> Y |- _ =>
match goal with
| z : Z |- _ => sselim_elim eq (f (g z))
end
end
| _ => fail "sselim: no hyp found"
end
| _ => fail "sselim: no eq found"
end;
nrapply paths_ind_r;
try clear eq;
try clear f.
Tactic Notation "sselim" constr(x0) := sselim x0.
Tactic Notation "sselim" constr(x0) constr(x1) := sselim x0; sselim x1.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) := sselim x0; sselim x1 x2.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) constr(x3) := sselim x0; sselim x1 x2 x3.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) := sselim x0; sselim x1 x2 x3 x4.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) constr(x5) := sselim x0; sselim x1 x2 x3 x4 x5.
Tactic Notation "sselim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) constr(x5) constr(x6) := sselim x0; sselim x1 x2 x3 x4 x5 x6.
Global Instance is01cat_ss : Is01Cat SuccStr.
exact (ap f (ss_fun_succ g x) @ ss_fun_succ f (g x)).
Global Instance is01cat_ssforall {A : SuccStr} (P : ssFam A)
: Is01Cat (ssForall P).
by destruct (ss_fun_succ f x).
by destruct (p x), (q x).
Global Instance is0gpd_ssforall {A : SuccStr} (P : ssFam A)
: Is0Gpd (ssForall P).
Global Instance is1cat_ss : Is1Cat SuccStr.
snrapply Build_Is0Functor.
destruct (p x); clear p; simpl.
snrapply Build_Is0Functor.