Library CatSem.CAT.simplicial_cat
Require Import Coq.Arith.Le Coq.Arith.Lt
Coq.Arith.Compare_dec.
Require Import Coq.Logic.ProofIrrelevance.
Require Export CatSem.CAT.functor.
Definition PI := proof_irrelevance.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Automatic Introduction.
Section N_set.
Variable n:nat.
Definition N_set:= {m | m < n}.
Definition projTT : N_set -> nat :=
fun x => proj1_sig x.
Coercion projTT : N_set >-> nat.
End N_set.
Notation "[[ n ]]" := (N_set n).
Section monotone_maps.
Inductive N_hom: nat -> nat -> Type :=
| empty: forall n, N_hom 0 n
| shift: forall n m, N_hom n (S m) -> N_hom (S n) (S m)
| lift: forall n m, N_hom (S n) m -> N_hom (S n) (S m).
Definition HomDelta (n m: nat) := N_hom n m.
Require Import Arith.
Definition monotone (m n: nat) (f: [[m]] -> [[n]]) :=
forall x y: [[m]], x <= y -> f x <= f y.
Definition interp: forall n m (f:HomDelta n m), [[n]] -> [[m]].
intros n m f x.
induction f.
unfold N_set in x.
elim x.
intros b c.
assert False.
apply (lt_n_O _ c).
elim H.
destruct x as [x p].
destruct x.
exists 0. auto with arith.
assert (H0: x < n).
apply lt_S_n.
assumption.
apply (IHf (exist (fun x => x < n) x H0)).
set (y := IHf x).
destruct y.
assert (H0: S x0 < S m).
apply lt_n_S.
assumption.
apply (exist (fun x => x < S m) (S x0) H0).
Defined.
Definition interp2: forall n m (f: HomDelta n m), [[n]] -> nat.
intros n m f x.
induction f.
elim x. intros x0 H.
assert False. apply (lt_n_O _ H). elim H0.
destruct x as [x p].
destruct x.
exact 0.
assert (H0: x < n).
apply lt_S_n. assumption.
apply (IHf (exist (fun x => x < n) x H0)).
exact (S (IHf x)).
Defined.
Section test.
Hypothesis H: 0 < S (S 0).
Definition test := shift (shift (empty 1)).
End test.
Lemma f_PI : forall m n (f: [[m]] -> [[n]]),
forall k l (H: k = l) pk pl,
f (exist _ k pk) = f (exist _ l pl).
Proof. intros m n f k l H.
rewrite H. intros pk pl. rewrite (PI _ pk pl).
auto.
Qed.
Lemma f_PI2 : forall m n (f: [[m]] -> [[n]]),
forall k pk pl r,
r = proj1_sig (f (existT _ k pk)) ->
r = proj1_sig (f (existT _ k pl)).
Proof. intros. simpl. rewrite <- (PI _ pk pl). auto.
Qed.
Lemma f_PI3 : forall m n (f: [[m]] -> [[n]]),
forall k pk pl,
f (exist _ k pk) = f (exist _ k pl).
Proof. intros m n f k pk pl.
rewrite <- (PI _ pk pl). auto.
Qed.
Lemma f_PI4: forall m n (f: [[m]] -> [[n]]),
forall k pk pl,
proj1_sig (f (exist _ k pk)) =
proj1_sig (f (exist _ k pl)).
Proof. intros. rewrite (f_PI3 f pk pl).
auto.
Qed.
Require Import Omega.
Lemma interp_monotone: forall m n (f: N_hom m n), monotone (interp f).
Proof. induction f.
unfold monotone. intro x. elim x.
intros x0 p.
assert (H': False). apply (lt_n_O x0 p).
elim H'.
unfold monotone. intros x y H.
destruct x as [x px].
destruct y as [y py]. simpl in *|-*.
destruct x. destruct y. simpl. auto.
simpl. omega.
destruct y. simpl. omega.
unfold monotone in IHf.
apply IHf. auto with arith.
unfold monotone. intros x y H. simpl.
assert (H': interp f x <= interp f y).
apply IHf. auto.
destruct (interp f x).
destruct (interp f y). simpl in *|-*.
auto with arith.
Qed.
Section translating_back.
Definition ins_0 (m:nat) : [[S m]] := exist (fun x => x < S m) 0
(lt_O_Sn m).
Program Definition unlift (m n: nat) (f: [[S m]] -> [[S n]])
(H: monotone f)
(H': f (ins_0 m) > 0) (x:[[S m]]) : [[n]] :=
pred (f x).
Next Obligation.
Proof.
simpl;
intros m n f H H0 x.
assert (Hx : 1 <= f x).
apply le_trans with (f (ins_0 m)).
assumption.
apply H. auto with arith.
assert (Hxx: f x < (S n)).
elim f.
intros. simpl. assumption.
assert (pred (f x) < f x).
apply lt_pred_n_n. apply Hx.
apply le_trans with (f x).
rewrite <- (@S_pred (f x) 0). auto with arith.
apply Hx. auto with arith.
Qed.
Lemma unlift_monotone (m n:nat)(f: [[S m]] -> [[S n]])
(H: monotone f)
(H': f (ins_0 m) > 0):
monotone (unlift H H').
Proof. unfold monotone. intros m n f H H' x y Hxy.
simpl.
apply le_pred. apply H. auto.
Qed.
Require Import Omega.
Program Definition unshift (m n: nat) (f: [[S m]] -> [[n]])
: [[m]] -> [[n]] :=
fun x => f (S x).
Next Obligation.
Proof.
intros m n f x.
elim x. intros.
simpl.
apply lt_n_S.
auto.
Qed.
Lemma unshift_monotone (m n: nat) (f: [[S m]] -> [[n]]) :
monotone f -> monotone (unshift f).
Proof. unfold monotone. intros m n f H x y Hxy.
unfold unshift. apply H. simpl. auto with arith.
Qed.
End translating_back.
End monotone_maps.
Coq.Arith.Compare_dec.
Require Import Coq.Logic.ProofIrrelevance.
Require Export CatSem.CAT.functor.
Definition PI := proof_irrelevance.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Automatic Introduction.
Section N_set.
Variable n:nat.
Definition N_set:= {m | m < n}.
Definition projTT : N_set -> nat :=
fun x => proj1_sig x.
Coercion projTT : N_set >-> nat.
End N_set.
Notation "[[ n ]]" := (N_set n).
Section monotone_maps.
Inductive N_hom: nat -> nat -> Type :=
| empty: forall n, N_hom 0 n
| shift: forall n m, N_hom n (S m) -> N_hom (S n) (S m)
| lift: forall n m, N_hom (S n) m -> N_hom (S n) (S m).
Definition HomDelta (n m: nat) := N_hom n m.
Require Import Arith.
Definition monotone (m n: nat) (f: [[m]] -> [[n]]) :=
forall x y: [[m]], x <= y -> f x <= f y.
Definition interp: forall n m (f:HomDelta n m), [[n]] -> [[m]].
intros n m f x.
induction f.
unfold N_set in x.
elim x.
intros b c.
assert False.
apply (lt_n_O _ c).
elim H.
destruct x as [x p].
destruct x.
exists 0. auto with arith.
assert (H0: x < n).
apply lt_S_n.
assumption.
apply (IHf (exist (fun x => x < n) x H0)).
set (y := IHf x).
destruct y.
assert (H0: S x0 < S m).
apply lt_n_S.
assumption.
apply (exist (fun x => x < S m) (S x0) H0).
Defined.
Definition interp2: forall n m (f: HomDelta n m), [[n]] -> nat.
intros n m f x.
induction f.
elim x. intros x0 H.
assert False. apply (lt_n_O _ H). elim H0.
destruct x as [x p].
destruct x.
exact 0.
assert (H0: x < n).
apply lt_S_n. assumption.
apply (IHf (exist (fun x => x < n) x H0)).
exact (S (IHf x)).
Defined.
Section test.
Hypothesis H: 0 < S (S 0).
Definition test := shift (shift (empty 1)).
End test.
Lemma f_PI : forall m n (f: [[m]] -> [[n]]),
forall k l (H: k = l) pk pl,
f (exist _ k pk) = f (exist _ l pl).
Proof. intros m n f k l H.
rewrite H. intros pk pl. rewrite (PI _ pk pl).
auto.
Qed.
Lemma f_PI2 : forall m n (f: [[m]] -> [[n]]),
forall k pk pl r,
r = proj1_sig (f (existT _ k pk)) ->
r = proj1_sig (f (existT _ k pl)).
Proof. intros. simpl. rewrite <- (PI _ pk pl). auto.
Qed.
Lemma f_PI3 : forall m n (f: [[m]] -> [[n]]),
forall k pk pl,
f (exist _ k pk) = f (exist _ k pl).
Proof. intros m n f k pk pl.
rewrite <- (PI _ pk pl). auto.
Qed.
Lemma f_PI4: forall m n (f: [[m]] -> [[n]]),
forall k pk pl,
proj1_sig (f (exist _ k pk)) =
proj1_sig (f (exist _ k pl)).
Proof. intros. rewrite (f_PI3 f pk pl).
auto.
Qed.
Require Import Omega.
Lemma interp_monotone: forall m n (f: N_hom m n), monotone (interp f).
Proof. induction f.
unfold monotone. intro x. elim x.
intros x0 p.
assert (H': False). apply (lt_n_O x0 p).
elim H'.
unfold monotone. intros x y H.
destruct x as [x px].
destruct y as [y py]. simpl in *|-*.
destruct x. destruct y. simpl. auto.
simpl. omega.
destruct y. simpl. omega.
unfold monotone in IHf.
apply IHf. auto with arith.
unfold monotone. intros x y H. simpl.
assert (H': interp f x <= interp f y).
apply IHf. auto.
destruct (interp f x).
destruct (interp f y). simpl in *|-*.
auto with arith.
Qed.
Section translating_back.
Definition ins_0 (m:nat) : [[S m]] := exist (fun x => x < S m) 0
(lt_O_Sn m).
Program Definition unlift (m n: nat) (f: [[S m]] -> [[S n]])
(H: monotone f)
(H': f (ins_0 m) > 0) (x:[[S m]]) : [[n]] :=
pred (f x).
Next Obligation.
Proof.
simpl;
intros m n f H H0 x.
assert (Hx : 1 <= f x).
apply le_trans with (f (ins_0 m)).
assumption.
apply H. auto with arith.
assert (Hxx: f x < (S n)).
elim f.
intros. simpl. assumption.
assert (pred (f x) < f x).
apply lt_pred_n_n. apply Hx.
apply le_trans with (f x).
rewrite <- (@S_pred (f x) 0). auto with arith.
apply Hx. auto with arith.
Qed.
Lemma unlift_monotone (m n:nat)(f: [[S m]] -> [[S n]])
(H: monotone f)
(H': f (ins_0 m) > 0):
monotone (unlift H H').
Proof. unfold monotone. intros m n f H H' x y Hxy.
simpl.
apply le_pred. apply H. auto.
Qed.
Require Import Omega.
Program Definition unshift (m n: nat) (f: [[S m]] -> [[n]])
: [[m]] -> [[n]] :=
fun x => f (S x).
Next Obligation.
Proof.
intros m n f x.
elim x. intros.
simpl.
apply lt_n_S.
auto.
Qed.
Lemma unshift_monotone (m n: nat) (f: [[S m]] -> [[n]]) :
monotone f -> monotone (unshift f).
Proof. unfold monotone. intros m n f H x y Hxy.
unfold unshift. apply H. simpl. auto with arith.
Qed.
End translating_back.
End monotone_maps.