mirror of https://github.com/nmvdw/HITs-Examples
Splitted cons_repr
This commit is contained in:
Niels
parent
5ee7053631
commit
2ccece3225
|
|
@ -4,14 +4,18 @@ lattice.v
|
||||||
disjunction.v
|
disjunction.v
|
||||||
representations/bad.v
|
representations/bad.v
|
||||||
representations/definition.v
|
representations/definition.v
|
||||||
|
representations/cons_repr.v
|
||||||
|
fsets/operations_cons_repr.v
|
||||||
|
fsets/properties_cons_repr.v
|
||||||
|
fsets/isomorphism.v
|
||||||
fsets/operations.v
|
fsets/operations.v
|
||||||
fsets/properties.v
|
fsets/properties.v
|
||||||
fsets/operations_decidable.v
|
fsets/operations_decidable.v
|
||||||
fsets/extensionality.v
|
fsets/extensionality.v
|
||||||
fsets/properties_decidable.v
|
fsets/properties_decidable.v
|
||||||
|
fsets/length.v
|
||||||
fsets/monad.v
|
fsets/monad.v
|
||||||
FSets.v
|
FSets.v
|
||||||
representations/cons_repr.v
|
|
||||||
implementations/lists.v
|
implementations/lists.v
|
||||||
variations/enumerated.v
|
variations/enumerated.v
|
||||||
#empty_set.v
|
#empty_set.v
|
||||||
|
|
|
||||||
|
|
@ -4,108 +4,108 @@ From representations Require Import definition.
|
||||||
From fsets Require Import operations properties.
|
From fsets Require Import operations properties.
|
||||||
|
|
||||||
Section ext.
|
Section ext.
|
||||||
Context {A : Type}.
|
Context {A : Type}.
|
||||||
Context `{Univalence}.
|
Context `{Univalence}.
|
||||||
|
|
||||||
Lemma subset_union_equiv
|
Lemma subset_union_equiv
|
||||||
: forall X Y : FSet A, subset X Y <~> U X Y = Y.
|
: forall X Y : FSet A, subset X Y <~> U X Y = Y.
|
||||||
Proof.
|
Proof.
|
||||||
intros X Y.
|
intros X Y.
|
||||||
eapply equiv_iff_hprop_uncurried.
|
eapply equiv_iff_hprop_uncurried.
|
||||||
split.
|
|
||||||
- apply subset_union.
|
|
||||||
- intro HXY.
|
|
||||||
rewrite <- HXY.
|
|
||||||
apply subset_union_l.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma subset_isIn (X Y : FSet A) :
|
|
||||||
(forall (a : A), isIn a X -> isIn a Y)
|
|
||||||
<~> (subset X Y).
|
|
||||||
Proof.
|
|
||||||
eapply equiv_iff_hprop_uncurried.
|
|
||||||
split.
|
|
||||||
- hinduction X ;
|
|
||||||
try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
|
|
||||||
+ intros ; reflexivity.
|
|
||||||
+ intros a f.
|
|
||||||
apply f.
|
|
||||||
apply tr ; reflexivity.
|
|
||||||
+ intros X1 X2 H1 H2 f.
|
|
||||||
enough (subset X1 Y).
|
|
||||||
enough (subset X2 Y).
|
|
||||||
{ split. apply X. apply X0. }
|
|
||||||
* apply H2.
|
|
||||||
intros a Ha.
|
|
||||||
apply f.
|
|
||||||
apply tr.
|
|
||||||
right.
|
|
||||||
apply Ha.
|
|
||||||
* apply H1.
|
|
||||||
intros a Ha.
|
|
||||||
apply f.
|
|
||||||
apply tr.
|
|
||||||
left.
|
|
||||||
apply Ha.
|
|
||||||
- hinduction X ;
|
|
||||||
try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
|
|
||||||
+ intros. contradiction.
|
|
||||||
+ intros b f a.
|
|
||||||
simple refine (Trunc_ind _ _) ; cbn.
|
|
||||||
intro p.
|
|
||||||
rewrite p^ in f.
|
|
||||||
apply f.
|
|
||||||
+ intros X1 X2 IH1 IH2 [H1 H2] a.
|
|
||||||
simple refine (Trunc_ind _ _) ; cbn.
|
|
||||||
intros [C1 | C2].
|
|
||||||
++ apply (IH1 H1 a C1).
|
|
||||||
++ apply (IH2 H2 a C2).
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
(** ** Extensionality proof *)
|
|
||||||
|
|
||||||
Lemma eq_subset' (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
|
|
||||||
Proof.
|
|
||||||
unshelve eapply BuildEquiv.
|
|
||||||
{ intro H'. rewrite H'. split; apply union_idem. }
|
|
||||||
unshelve esplit.
|
|
||||||
{ intros [H1 H2]. etransitivity. apply H1^.
|
|
||||||
rewrite comm. apply H2. }
|
|
||||||
intro; apply path_prod; apply set_path2.
|
|
||||||
all: intro; apply set_path2.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma eq_subset (X Y : FSet A) :
|
|
||||||
X = Y <~> (subset Y X * subset X Y).
|
|
||||||
Proof.
|
|
||||||
transitivity ((U Y X = X) * (U X Y = Y)).
|
|
||||||
apply eq_subset'.
|
|
||||||
symmetry.
|
|
||||||
eapply equiv_functor_prod'; apply subset_union_equiv.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Theorem fset_ext (X Y : FSet A) :
|
|
||||||
X = Y <~> (forall (a : A), isIn a X = isIn a Y).
|
|
||||||
Proof.
|
|
||||||
refine (@equiv_compose' _ _ _ _ _) ; [ | apply eq_subset ].
|
|
||||||
refine (@equiv_compose' _ ((forall a, isIn a Y -> isIn a X)
|
|
||||||
*(forall a, isIn a X -> isIn a Y)) _ _ _).
|
|
||||||
- apply equiv_iff_hprop_uncurried.
|
|
||||||
split.
|
split.
|
||||||
* intros [H1 H2 a].
|
- apply subset_union.
|
||||||
specialize (H1 a) ; specialize (H2 a).
|
- intro HXY.
|
||||||
apply path_iff_hprop.
|
rewrite <- HXY.
|
||||||
apply H2.
|
apply subset_union_l.
|
||||||
apply H1.
|
Defined.
|
||||||
* intros H1.
|
|
||||||
split ; intro a ; intro H2.
|
Lemma subset_isIn (X Y : FSet A) :
|
||||||
|
(forall (a : A), isIn a X -> isIn a Y)
|
||||||
|
<~> (subset X Y).
|
||||||
|
Proof.
|
||||||
|
eapply equiv_iff_hprop_uncurried.
|
||||||
|
split.
|
||||||
|
- hinduction X ;
|
||||||
|
try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
|
||||||
|
+ intros ; reflexivity.
|
||||||
|
+ intros a f.
|
||||||
|
apply f.
|
||||||
|
apply tr ; reflexivity.
|
||||||
|
+ intros X1 X2 H1 H2 f.
|
||||||
|
enough (subset X1 Y).
|
||||||
|
enough (subset X2 Y).
|
||||||
|
{ split. apply X. apply X0. }
|
||||||
|
* apply H2.
|
||||||
|
intros a Ha.
|
||||||
|
apply f.
|
||||||
|
apply tr.
|
||||||
|
right.
|
||||||
|
apply Ha.
|
||||||
|
* apply H1.
|
||||||
|
intros a Ha.
|
||||||
|
apply f.
|
||||||
|
apply tr.
|
||||||
|
left.
|
||||||
|
apply Ha.
|
||||||
|
- hinduction X ;
|
||||||
|
try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
|
||||||
|
+ intros. contradiction.
|
||||||
|
+ intros b f a.
|
||||||
|
simple refine (Trunc_ind _ _) ; cbn.
|
||||||
|
intro p.
|
||||||
|
rewrite p^ in f.
|
||||||
|
apply f.
|
||||||
|
+ intros X1 X2 IH1 IH2 [H1 H2] a.
|
||||||
|
simple refine (Trunc_ind _ _) ; cbn.
|
||||||
|
intros [C1 | C2].
|
||||||
|
++ apply (IH1 H1 a C1).
|
||||||
|
++ apply (IH2 H2 a C2).
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
(** ** Extensionality proof *)
|
||||||
|
|
||||||
|
Lemma eq_subset' (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
|
||||||
|
Proof.
|
||||||
|
unshelve eapply BuildEquiv.
|
||||||
|
{ intro H'. rewrite H'. split; apply union_idem. }
|
||||||
|
unshelve esplit.
|
||||||
|
{ intros [H1 H2]. etransitivity. apply H1^.
|
||||||
|
rewrite comm. apply H2. }
|
||||||
|
intro; apply path_prod; apply set_path2.
|
||||||
|
all: intro; apply set_path2.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma eq_subset (X Y : FSet A) :
|
||||||
|
X = Y <~> (subset Y X * subset X Y).
|
||||||
|
Proof.
|
||||||
|
transitivity ((U Y X = X) * (U X Y = Y)).
|
||||||
|
apply eq_subset'.
|
||||||
|
symmetry.
|
||||||
|
eapply equiv_functor_prod'; apply subset_union_equiv.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Theorem fset_ext (X Y : FSet A) :
|
||||||
|
X = Y <~> (forall (a : A), isIn a X = isIn a Y).
|
||||||
|
Proof.
|
||||||
|
refine (@equiv_compose' _ _ _ _ _) ; [ | apply eq_subset ].
|
||||||
|
refine (@equiv_compose' _ ((forall a, isIn a Y -> isIn a X)
|
||||||
|
*(forall a, isIn a X -> isIn a Y)) _ _ _).
|
||||||
|
- apply equiv_iff_hprop_uncurried.
|
||||||
|
split.
|
||||||
|
* intros [H1 H2 a].
|
||||||
|
specialize (H1 a) ; specialize (H2 a).
|
||||||
|
apply path_iff_hprop.
|
||||||
|
apply H2.
|
||||||
|
apply H1.
|
||||||
|
* intros H1.
|
||||||
|
split ; intro a ; intro H2.
|
||||||
+ rewrite (H1 a).
|
+ rewrite (H1 a).
|
||||||
apply H2.
|
apply H2.
|
||||||
+ rewrite <- (H1 a).
|
+ rewrite <- (H1 a).
|
||||||
apply H2.
|
apply H2.
|
||||||
- eapply equiv_functor_prod' ;
|
- eapply equiv_functor_prod' ;
|
||||||
apply equiv_iff_hprop_uncurried ;
|
apply equiv_iff_hprop_uncurried ;
|
||||||
split ; apply subset_isIn.
|
split ; apply subset_isIn.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
End ext.
|
End ext.
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,69 @@
|
||||||
|
(* The representations [FSet A] and [FSetC A] are isomorphic for every A *)
|
||||||
|
Require Import HoTT HitTactics.
|
||||||
|
From representations Require Import cons_repr definition.
|
||||||
|
From fsets Require Import operations_cons_repr properties_cons_repr.
|
||||||
|
|
||||||
|
Section Iso.
|
||||||
|
|
||||||
|
Context {A : Type}.
|
||||||
|
Context `{Univalence}.
|
||||||
|
|
||||||
|
Definition FSetC_to_FSet: FSetC A -> FSet A.
|
||||||
|
Proof.
|
||||||
|
hrecursion.
|
||||||
|
- apply E.
|
||||||
|
- intros a x. apply (U (L a) x).
|
||||||
|
- intros. cbn.
|
||||||
|
etransitivity. apply assoc.
|
||||||
|
apply (ap (fun y => U y x)).
|
||||||
|
apply idem.
|
||||||
|
- intros. cbn.
|
||||||
|
etransitivity. apply assoc.
|
||||||
|
etransitivity. refine (ap (fun y => U y x) _ ).
|
||||||
|
apply FSet.comm.
|
||||||
|
symmetry.
|
||||||
|
apply assoc.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Definition FSet_to_FSetC: FSet A -> FSetC A :=
|
||||||
|
FSet_rec A (FSetC A) (FSetC.trunc A) Nil singleton append append_assoc
|
||||||
|
append_comm append_nl append_nr singleton_idem.
|
||||||
|
|
||||||
|
Lemma append_union: forall (x y: FSetC A),
|
||||||
|
FSetC_to_FSet (append x y) = U (FSetC_to_FSet x) (FSetC_to_FSet y).
|
||||||
|
Proof.
|
||||||
|
intros x.
|
||||||
|
hrecursion x; try (intros; apply path_forall; intro; apply set_path2).
|
||||||
|
- intros. symmetry. apply nl.
|
||||||
|
- intros a x HR y. rewrite HR. apply assoc.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma repr_iso_id_l: forall (x: FSet A), FSetC_to_FSet (FSet_to_FSetC x) = x.
|
||||||
|
Proof.
|
||||||
|
hinduction; try (intros; apply set_path2).
|
||||||
|
- reflexivity.
|
||||||
|
- intro. apply nr.
|
||||||
|
- intros x y p q. rewrite append_union, p, q. reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
Lemma repr_iso_id_r: forall (x: FSetC A), FSet_to_FSetC (FSetC_to_FSet x) = x.
|
||||||
|
Proof.
|
||||||
|
hinduction; try (intros; apply set_path2).
|
||||||
|
- reflexivity.
|
||||||
|
- intros a x HR. rewrite HR. reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem repr_iso: FSet A <~> FSetC A.
|
||||||
|
Proof.
|
||||||
|
simple refine (@BuildEquiv (FSet A) (FSetC A) FSet_to_FSetC _ ).
|
||||||
|
apply isequiv_biinv.
|
||||||
|
unfold BiInv. split.
|
||||||
|
exists FSetC_to_FSet.
|
||||||
|
unfold Sect. apply repr_iso_id_l.
|
||||||
|
exists FSetC_to_FSet.
|
||||||
|
unfold Sect. apply repr_iso_id_r.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
End Iso.
|
||||||
|
|
@ -0,0 +1,40 @@
|
||||||
|
(* The length function for finite sets *)
|
||||||
|
Require Import HoTT HitTactics.
|
||||||
|
From representations Require Import cons_repr definition.
|
||||||
|
From fsets Require Import operations_decidable isomorphism properties_decidable.
|
||||||
|
|
||||||
|
Section Length.
|
||||||
|
|
||||||
|
Context {A : Type}.
|
||||||
|
Context {A_deceq : DecidablePaths A}.
|
||||||
|
Context `{Univalence}.
|
||||||
|
|
||||||
|
Opaque isIn_b.
|
||||||
|
|
||||||
|
Definition length (x: FSetC A) : nat.
|
||||||
|
Proof.
|
||||||
|
simple refine (FSetC_ind A _ _ _ _ _ _ x ); simpl.
|
||||||
|
- exact 0.
|
||||||
|
- intros a y n.
|
||||||
|
pose (y' := FSetC_to_FSet y).
|
||||||
|
exact (if isIn_b a y' then n else (S n)).
|
||||||
|
- intros. rewrite transport_const. cbn.
|
||||||
|
simplify_isIn. simpl. reflexivity.
|
||||||
|
- intros. rewrite transport_const. cbn.
|
||||||
|
simplify_isIn.
|
||||||
|
destruct (dec (a = b)) as [Hab | Hab].
|
||||||
|
+ rewrite Hab. simplify_isIn. simpl. reflexivity.
|
||||||
|
+ rewrite ?L_isIn_b_false; auto. simpl.
|
||||||
|
destruct (isIn_b a (FSetC_to_FSet x0)), (isIn_b b (FSetC_to_FSet x0)) ; reflexivity.
|
||||||
|
intro p. contradiction (Hab p^).
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Definition length_FSet (x: FSet A) := length (FSet_to_FSetC x).
|
||||||
|
|
||||||
|
Lemma length_singleton: forall (a: A), length_FSet (L a) = 1.
|
||||||
|
Proof.
|
||||||
|
intro a.
|
||||||
|
cbn. reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
End Length.
|
||||||
|
|
@ -0,0 +1,19 @@
|
||||||
|
(* Operations on [FSetC A] *)
|
||||||
|
Require Import HoTT HitTactics.
|
||||||
|
Require Import representations.cons_repr.
|
||||||
|
|
||||||
|
Section operations.
|
||||||
|
|
||||||
|
Context {A : Type}.
|
||||||
|
|
||||||
|
Definition append (x y: FSetC A) : FSetC A.
|
||||||
|
hinduction x.
|
||||||
|
- apply y.
|
||||||
|
- apply Cns.
|
||||||
|
- apply dupl.
|
||||||
|
- apply comm.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Definition singleton (a:A) : FSetC A := a;;∅.
|
||||||
|
|
||||||
|
End operations.
|
||||||
|
|
@ -0,0 +1,75 @@
|
||||||
|
(* Properties of the operations on [FSetC A] *)
|
||||||
|
Require Import HoTT HitTactics.
|
||||||
|
Require Import representations.cons_repr.
|
||||||
|
From fsets Require Import operations_cons_repr.
|
||||||
|
|
||||||
|
Section properties.
|
||||||
|
Context {A : Type}.
|
||||||
|
|
||||||
|
Lemma append_nl:
|
||||||
|
forall (x: FSetC A), append ∅ x = x.
|
||||||
|
Proof.
|
||||||
|
intro. reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma append_nr:
|
||||||
|
forall (x: FSetC A), append x ∅ = x.
|
||||||
|
Proof.
|
||||||
|
hinduction; try (intros; apply set_path2).
|
||||||
|
- reflexivity.
|
||||||
|
- intros. apply (ap (fun y => a ;; y) X).
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma append_assoc {H: Funext}:
|
||||||
|
forall (x y z: FSetC A), append x (append y z) = append (append x y) z.
|
||||||
|
Proof.
|
||||||
|
intro x; hinduction x; try (intros; apply set_path2).
|
||||||
|
- reflexivity.
|
||||||
|
- intros a x HR y z.
|
||||||
|
specialize (HR y z).
|
||||||
|
apply (ap (fun y => a ;; y) HR).
|
||||||
|
- intros. apply path_forall.
|
||||||
|
intro. apply path_forall.
|
||||||
|
intro. apply set_path2.
|
||||||
|
- intros. apply path_forall.
|
||||||
|
intro. apply path_forall.
|
||||||
|
intro. apply set_path2.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma append_singleton: forall (a: A) (x: FSetC A),
|
||||||
|
a ;; x = append x (a ;; ∅).
|
||||||
|
Proof.
|
||||||
|
intro a. hinduction; try (intros; apply set_path2).
|
||||||
|
- reflexivity.
|
||||||
|
- intros b x HR. refine (_ @ _).
|
||||||
|
+ apply comm.
|
||||||
|
+ apply (ap (fun y => b ;; y) HR).
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma append_comm {H: Funext}:
|
||||||
|
forall (x1 x2: FSetC A), append x1 x2 = append x2 x1.
|
||||||
|
Proof.
|
||||||
|
intro x1.
|
||||||
|
hinduction x1; try (intros; apply set_path2).
|
||||||
|
- intros. symmetry. apply append_nr.
|
||||||
|
- intros a x1 HR x2.
|
||||||
|
etransitivity.
|
||||||
|
apply (ap (fun y => a;;y) (HR x2)).
|
||||||
|
transitivity (append (append x2 x1) (a;;∅)).
|
||||||
|
+ apply append_singleton.
|
||||||
|
+ etransitivity.
|
||||||
|
* symmetry. apply append_assoc.
|
||||||
|
* simple refine (ap (fun y => append x2 y) (append_singleton _ _)^).
|
||||||
|
- intros. apply path_forall.
|
||||||
|
intro. apply set_path2.
|
||||||
|
- intros. apply path_forall.
|
||||||
|
intro. apply set_path2.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma singleton_idem: forall (a: A),
|
||||||
|
append (singleton a) (singleton a) = singleton a.
|
||||||
|
Proof.
|
||||||
|
unfold singleton. intro. cbn. apply dupl.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
End properties.
|
||||||
|
|
@ -1,5 +1,7 @@
|
||||||
|
(* Implementation of [FSet A] using lists *)
|
||||||
Require Import HoTT HitTactics.
|
Require Import HoTT HitTactics.
|
||||||
Require Import representations.cons_repr FSets.
|
Require Import representations.cons_repr FSets.
|
||||||
|
From fsets Require Import operations_cons_repr isomorphism length.
|
||||||
|
|
||||||
Section Operations.
|
Section Operations.
|
||||||
Variable A : Type.
|
Variable A : Type.
|
||||||
|
|
@ -80,7 +82,7 @@ Section ListToSet.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma append_FSetCappend (l1 l2 : list A) :
|
Lemma append_FSetCappend (l1 l2 : list A) :
|
||||||
list_to_setC (append l1 l2) = FSetC.append (list_to_setC l1) (list_to_setC l2).
|
list_to_setC (append l1 l2) = operations_cons_repr.append (list_to_setC l1) (list_to_setC l2).
|
||||||
Proof.
|
Proof.
|
||||||
induction l1 ; simpl in *.
|
induction l1 ; simpl in *.
|
||||||
- reflexivity.
|
- reflexivity.
|
||||||
|
|
@ -117,7 +119,7 @@ Section ListToSet.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma length_sizeC (l : list A) :
|
Lemma length_sizeC (l : list A) :
|
||||||
cardinality l = cons_repr.length (list_to_setC l).
|
cardinality l = length (list_to_setC l).
|
||||||
Proof.
|
Proof.
|
||||||
induction l.
|
induction l.
|
||||||
- cbn.
|
- cbn.
|
||||||
|
|
|
||||||
|
|
@ -5,187 +5,187 @@ Require Import HoTT.
|
||||||
Require Import HitTactics.
|
Require Import HitTactics.
|
||||||
Module Export FSet.
|
Module Export FSet.
|
||||||
|
|
||||||
Section FSet.
|
Section FSet.
|
||||||
Variable A : Type.
|
Variable A : Type.
|
||||||
|
|
||||||
Private Inductive FSet : Type :=
|
Private Inductive FSet : Type :=
|
||||||
| E : FSet
|
| E : FSet
|
||||||
| L : A -> FSet
|
| L : A -> FSet
|
||||||
| U : FSet -> FSet -> FSet.
|
| U : FSet -> FSet -> FSet.
|
||||||
|
|
||||||
Notation "{| x |}" := (L x).
|
Notation "{| x |}" := (L x).
|
||||||
Infix "∪" := U (at level 8, right associativity).
|
Infix "∪" := U (at level 8, right associativity).
|
||||||
Notation "∅" := E.
|
Notation "∅" := E.
|
||||||
|
|
||||||
Axiom assoc : forall (x y z : FSet ),
|
Axiom assoc : forall (x y z : FSet ),
|
||||||
x ∪ (y ∪ z) = (x ∪ y) ∪ z.
|
x ∪ (y ∪ z) = (x ∪ y) ∪ z.
|
||||||
|
|
||||||
Axiom comm : forall (x y : FSet),
|
Axiom comm : forall (x y : FSet),
|
||||||
x ∪ y = y ∪ x.
|
x ∪ y = y ∪ x.
|
||||||
|
|
||||||
Axiom nl : forall (x : FSet),
|
Axiom nl : forall (x : FSet),
|
||||||
∅ ∪ x = x.
|
∅ ∪ x = x.
|
||||||
|
|
||||||
Axiom nr : forall (x : FSet),
|
Axiom nr : forall (x : FSet),
|
||||||
x ∪ ∅ = x.
|
x ∪ ∅ = x.
|
||||||
|
|
||||||
Axiom idem : forall (x : A),
|
Axiom idem : forall (x : A),
|
||||||
{| x |} ∪ {|x|} = {|x|}.
|
{| x |} ∪ {|x|} = {|x|}.
|
||||||
|
|
||||||
End FSet.
|
End FSet.
|
||||||
|
|
||||||
Arguments E {_}.
|
Arguments E {_}.
|
||||||
Arguments U {_} _ _.
|
Arguments U {_} _ _.
|
||||||
Arguments L {_} _.
|
Arguments L {_} _.
|
||||||
Arguments assoc {_} _ _ _.
|
Arguments assoc {_} _ _ _.
|
||||||
Arguments comm {_} _ _.
|
Arguments comm {_} _ _.
|
||||||
Arguments nl {_} _.
|
Arguments nl {_} _.
|
||||||
Arguments nr {_} _.
|
Arguments nr {_} _.
|
||||||
Arguments idem {_} _.
|
Arguments idem {_} _.
|
||||||
|
|
||||||
Section FSet_induction.
|
Section FSet_induction.
|
||||||
Variable A: Type.
|
Variable A: Type.
|
||||||
Variable (P : FSet A -> Type).
|
Variable (P : FSet A -> Type).
|
||||||
Variable (eP : P E).
|
Variable (eP : P E).
|
||||||
Variable (lP : forall a: A, P (L a)).
|
Variable (lP : forall a: A, P (L a)).
|
||||||
Variable (uP : forall (x y: FSet A), P x -> P y -> P (U x y)).
|
Variable (uP : forall (x y: FSet A), P x -> P y -> P (U x y)).
|
||||||
Variable (assocP : forall (x y z : FSet A)
|
Variable (assocP : forall (x y z : FSet A)
|
||||||
(px: P x) (py: P y) (pz: P z),
|
(px: P x) (py: P y) (pz: P z),
|
||||||
assoc x y z #
|
assoc x y z #
|
||||||
(uP x (U y z) px (uP y z py pz))
|
(uP x (U y z) px (uP y z py pz))
|
||||||
=
|
=
|
||||||
(uP (U x y) z (uP x y px py) pz)).
|
(uP (U x y) z (uP x y px py) pz)).
|
||||||
Variable (commP : forall (x y: FSet A) (px: P x) (py: P y),
|
Variable (commP : forall (x y: FSet A) (px: P x) (py: P y),
|
||||||
comm x y #
|
comm x y #
|
||||||
uP x y px py = uP y x py px).
|
uP x y px py = uP y x py px).
|
||||||
Variable (nlP : forall (x : FSet A) (px: P x),
|
Variable (nlP : forall (x : FSet A) (px: P x),
|
||||||
nl x # uP E x eP px = px).
|
nl x # uP E x eP px = px).
|
||||||
Variable (nrP : forall (x : FSet A) (px: P x),
|
Variable (nrP : forall (x : FSet A) (px: P x),
|
||||||
nr x # uP x E px eP = px).
|
nr x # uP x E px eP = px).
|
||||||
Variable (idemP : forall (x : A),
|
Variable (idemP : forall (x : A),
|
||||||
idem x # uP (L x) (L x) (lP x) (lP x) = lP x).
|
idem x # uP (L x) (L x) (lP x) (lP x) = lP x).
|
||||||
|
|
||||||
(* Induction principle *)
|
(* Induction principle *)
|
||||||
Fixpoint FSet_ind
|
Fixpoint FSet_ind
|
||||||
(x : FSet A)
|
(x : FSet A)
|
||||||
{struct x}
|
{struct x}
|
||||||
: P x
|
: P x
|
||||||
:= (match x return _ -> _ -> _ -> _ -> _ -> P x with
|
:= (match x return _ -> _ -> _ -> _ -> _ -> P x with
|
||||||
| E => fun _ => fun _ => fun _ => fun _ => fun _ => eP
|
| E => fun _ => fun _ => fun _ => fun _ => fun _ => eP
|
||||||
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
|
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
|
||||||
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
|
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
|
||||||
(FSet_ind y)
|
(FSet_ind y)
|
||||||
(FSet_ind z)
|
(FSet_ind z)
|
||||||
end) assocP commP nlP nrP idemP.
|
end) assocP commP nlP nrP idemP.
|
||||||
|
|
||||||
|
|
||||||
Axiom FSet_ind_beta_assoc : forall (x y z : FSet A),
|
Axiom FSet_ind_beta_assoc : forall (x y z : FSet A),
|
||||||
apD FSet_ind (assoc x y z) =
|
apD FSet_ind (assoc x y z) =
|
||||||
(assocP x y z (FSet_ind x) (FSet_ind y) (FSet_ind z)).
|
(assocP x y z (FSet_ind x) (FSet_ind y) (FSet_ind z)).
|
||||||
|
|
||||||
Axiom FSet_ind_beta_comm : forall (x y : FSet A),
|
Axiom FSet_ind_beta_comm : forall (x y : FSet A),
|
||||||
apD FSet_ind (comm x y) = (commP x y (FSet_ind x) (FSet_ind y)).
|
apD FSet_ind (comm x y) = (commP x y (FSet_ind x) (FSet_ind y)).
|
||||||
|
|
||||||
Axiom FSet_ind_beta_nl : forall (x : FSet A),
|
Axiom FSet_ind_beta_nl : forall (x : FSet A),
|
||||||
apD FSet_ind (nl x) = (nlP x (FSet_ind x)).
|
apD FSet_ind (nl x) = (nlP x (FSet_ind x)).
|
||||||
|
|
||||||
Axiom FSet_ind_beta_nr : forall (x : FSet A),
|
Axiom FSet_ind_beta_nr : forall (x : FSet A),
|
||||||
apD FSet_ind (nr x) = (nrP x (FSet_ind x)).
|
apD FSet_ind (nr x) = (nrP x (FSet_ind x)).
|
||||||
|
|
||||||
Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x.
|
Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x.
|
||||||
End FSet_induction.
|
End FSet_induction.
|
||||||
|
|
||||||
Section FSet_recursion.
|
Section FSet_recursion.
|
||||||
|
|
||||||
Variable A : Type.
|
Variable A : Type.
|
||||||
Variable P : Type.
|
Variable P : Type.
|
||||||
Variable e : P.
|
Variable e : P.
|
||||||
Variable l : A -> P.
|
Variable l : A -> P.
|
||||||
Variable u : P -> P -> P.
|
Variable u : P -> P -> P.
|
||||||
Variable assocP : forall (x y z : P), u x (u y z) = u (u x y) z.
|
Variable assocP : forall (x y z : P), u x (u y z) = u (u x y) z.
|
||||||
Variable commP : forall (x y : P), u x y = u y x.
|
Variable commP : forall (x y : P), u x y = u y x.
|
||||||
Variable nlP : forall (x : P), u e x = x.
|
Variable nlP : forall (x : P), u e x = x.
|
||||||
Variable nrP : forall (x : P), u x e = x.
|
Variable nrP : forall (x : P), u x e = x.
|
||||||
Variable idemP : forall (x : A), u (l x) (l x) = l x.
|
Variable idemP : forall (x : A), u (l x) (l x) = l x.
|
||||||
|
|
||||||
Definition FSet_rec : FSet A -> P.
|
Definition FSet_rec : FSet A -> P.
|
||||||
Proof.
|
Proof.
|
||||||
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _) ; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn.
|
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _) ; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn.
|
||||||
- apply e.
|
- apply e.
|
||||||
- apply l.
|
- apply l.
|
||||||
- intros x y ; apply u.
|
- intros x y ; apply u.
|
||||||
- apply assocP.
|
- apply assocP.
|
||||||
- apply commP.
|
- apply commP.
|
||||||
- apply nlP.
|
- apply nlP.
|
||||||
- apply nrP.
|
- apply nrP.
|
||||||
- apply idemP.
|
- apply idemP.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec_beta_assoc : forall (x y z : FSet A),
|
Definition FSet_rec_beta_assoc : forall (x y z : FSet A),
|
||||||
ap FSet_rec (assoc x y z)
|
ap FSet_rec (assoc x y z)
|
||||||
=
|
=
|
||||||
assocP (FSet_rec x) (FSet_rec y) (FSet_rec z).
|
assocP (FSet_rec x) (FSet_rec y) (FSet_rec z).
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
unfold FSet_rec.
|
unfold FSet_rec.
|
||||||
eapply (cancelL (transport_const (assoc x y z) _)).
|
eapply (cancelL (transport_const (assoc x y z) _)).
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
apply FSet_ind_beta_assoc.
|
apply FSet_ind_beta_assoc.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec_beta_comm : forall (x y : FSet A),
|
Definition FSet_rec_beta_comm : forall (x y : FSet A),
|
||||||
ap FSet_rec (comm x y)
|
ap FSet_rec (comm x y)
|
||||||
=
|
=
|
||||||
commP (FSet_rec x) (FSet_rec y).
|
commP (FSet_rec x) (FSet_rec y).
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
unfold FSet_rec.
|
unfold FSet_rec.
|
||||||
eapply (cancelL (transport_const (comm x y) _)).
|
eapply (cancelL (transport_const (comm x y) _)).
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
apply FSet_ind_beta_comm.
|
apply FSet_ind_beta_comm.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec_beta_nl : forall (x : FSet A),
|
Definition FSet_rec_beta_nl : forall (x : FSet A),
|
||||||
ap FSet_rec (nl x)
|
ap FSet_rec (nl x)
|
||||||
=
|
=
|
||||||
nlP (FSet_rec x).
|
nlP (FSet_rec x).
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
unfold FSet_rec.
|
unfold FSet_rec.
|
||||||
eapply (cancelL (transport_const (nl x) _)).
|
eapply (cancelL (transport_const (nl x) _)).
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
apply FSet_ind_beta_nl.
|
apply FSet_ind_beta_nl.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec_beta_nr : forall (x : FSet A),
|
Definition FSet_rec_beta_nr : forall (x : FSet A),
|
||||||
ap FSet_rec (nr x)
|
ap FSet_rec (nr x)
|
||||||
=
|
=
|
||||||
nrP (FSet_rec x).
|
nrP (FSet_rec x).
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
unfold FSet_rec.
|
unfold FSet_rec.
|
||||||
eapply (cancelL (transport_const (nr x) _)).
|
eapply (cancelL (transport_const (nr x) _)).
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
apply FSet_ind_beta_nr.
|
apply FSet_ind_beta_nr.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec_beta_idem : forall (a : A),
|
Definition FSet_rec_beta_idem : forall (a : A),
|
||||||
ap FSet_rec (idem a)
|
ap FSet_rec (idem a)
|
||||||
=
|
=
|
||||||
idemP a.
|
idemP a.
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
unfold FSet_rec.
|
unfold FSet_rec.
|
||||||
eapply (cancelL (transport_const (idem a) _)).
|
eapply (cancelL (transport_const (idem a) _)).
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
apply FSet_ind_beta_idem.
|
apply FSet_ind_beta_idem.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
End FSet_recursion.
|
End FSet_recursion.
|
||||||
|
|
||||||
Instance FSet_recursion A : HitRecursion (FSet A) := {
|
Instance FSet_recursion A : HitRecursion (FSet A) := {
|
||||||
indTy := _; recTy := _;
|
indTy := _; recTy := _;
|
||||||
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
|
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
|
||||||
|
|
||||||
End FSet.
|
End FSet.
|
||||||
|
|
||||||
|
|
@ -194,104 +194,104 @@ Infix "∪" := U (at level 8, right associativity).
|
||||||
Notation "∅" := E.
|
Notation "∅" := E.
|
||||||
|
|
||||||
Section set_sphere.
|
Section set_sphere.
|
||||||
From HoTT.HIT Require Import Circle.
|
From HoTT.HIT Require Import Circle.
|
||||||
From HoTT Require Import UnivalenceAxiom.
|
From HoTT Require Import UnivalenceAxiom.
|
||||||
Instance S1_recursion : HitRecursion S1 := {
|
Instance S1_recursion : HitRecursion S1 := {
|
||||||
indTy := _; recTy := _;
|
indTy := _; recTy := _;
|
||||||
H_inductor := S1_ind; H_recursor := S1_rec }.
|
H_inductor := S1_ind; H_recursor := S1_rec }.
|
||||||
|
|
||||||
Variable A : Type.
|
Variable A : Type.
|
||||||
|
|
||||||
Definition f (x : S1) : x = x.
|
Definition f (x : S1) : x = x.
|
||||||
Proof.
|
Proof.
|
||||||
hrecursion x.
|
hrecursion x.
|
||||||
- exact loop.
|
- exact loop.
|
||||||
- etransitivity.
|
- etransitivity.
|
||||||
eapply (@transport_paths_FlFr S1 S1 idmap idmap).
|
eapply (@transport_paths_FlFr S1 S1 idmap idmap).
|
||||||
hott_simpl.
|
hott_simpl.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition S1op (x y : S1) : S1.
|
Definition S1op (x y : S1) : S1.
|
||||||
Proof.
|
Proof.
|
||||||
hrecursion y.
|
hrecursion y.
|
||||||
- exact x. (* x + base = x *)
|
- exact x. (* x + base = x *)
|
||||||
- apply f.
|
- apply f.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma S1op_nr (x : S1) : S1op x base = x.
|
Lemma S1op_nr (x : S1) : S1op x base = x.
|
||||||
Proof. reflexivity. Defined.
|
Proof. reflexivity. Defined.
|
||||||
|
|
||||||
Lemma S1op_nl (x : S1) : S1op base x = x.
|
Lemma S1op_nl (x : S1) : S1op base x = x.
|
||||||
Proof.
|
Proof.
|
||||||
hrecursion x.
|
hrecursion x.
|
||||||
- exact loop.
|
- exact loop.
|
||||||
- etransitivity.
|
- etransitivity.
|
||||||
apply (@transport_paths_FlFr _ _ (fun x => S1op base x) idmap _ _ loop loop).
|
apply (@transport_paths_FlFr _ _ (fun x => S1op base x) idmap _ _ loop loop).
|
||||||
hott_simpl.
|
hott_simpl.
|
||||||
apply moveR_pM. apply moveR_pM. hott_simpl.
|
apply moveR_pM. apply moveR_pM. hott_simpl.
|
||||||
etransitivity. apply (ap_V (S1op base) loop).
|
etransitivity. apply (ap_V (S1op base) loop).
|
||||||
f_ap. apply S1_rec_beta_loop.
|
f_ap. apply S1_rec_beta_loop.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma S1op_assoc (x y z : S1) : S1op x (S1op y z) = S1op (S1op x y) z.
|
Lemma S1op_assoc (x y z : S1) : S1op x (S1op y z) = S1op (S1op x y) z.
|
||||||
Proof.
|
Proof.
|
||||||
hrecursion z.
|
hrecursion z.
|
||||||
- reflexivity.
|
- reflexivity.
|
||||||
- etransitivity.
|
- etransitivity.
|
||||||
apply (@transport_paths_FlFr _ _ (fun z => S1op x (S1op y z)) (S1op (S1op x y)) _ _ loop idpath).
|
apply (@transport_paths_FlFr _ _ (fun z => S1op x (S1op y z)) (S1op (S1op x y)) _ _ loop idpath).
|
||||||
hott_simpl.
|
hott_simpl.
|
||||||
apply moveR_Mp. hott_simpl.
|
apply moveR_Mp. hott_simpl.
|
||||||
rewrite S1_rec_beta_loop.
|
rewrite S1_rec_beta_loop.
|
||||||
rewrite ap_compose.
|
rewrite ap_compose.
|
||||||
rewrite S1_rec_beta_loop.
|
rewrite S1_rec_beta_loop.
|
||||||
hrecursion y.
|
hrecursion y.
|
||||||
+ symmetry. apply S1_rec_beta_loop.
|
+ symmetry. apply S1_rec_beta_loop.
|
||||||
+ apply is1type_S1.
|
+ apply is1type_S1.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma S1op_comm (x y : S1) : S1op x y = S1op y x.
|
Lemma S1op_comm (x y : S1) : S1op x y = S1op y x.
|
||||||
Proof.
|
Proof.
|
||||||
hrecursion x.
|
hrecursion x.
|
||||||
- apply S1op_nl.
|
- apply S1op_nl.
|
||||||
- hrecursion y.
|
- hrecursion y.
|
||||||
+ rewrite transport_paths_FlFr. hott_simpl.
|
+ rewrite transport_paths_FlFr. hott_simpl.
|
||||||
rewrite S1_rec_beta_loop. reflexivity.
|
rewrite S1_rec_beta_loop. reflexivity.
|
||||||
+ apply is1type_S1.
|
+ apply is1type_S1.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_to_S : FSet A -> S1.
|
Definition FSet_to_S : FSet A -> S1.
|
||||||
Proof.
|
Proof.
|
||||||
hrecursion.
|
hrecursion.
|
||||||
- exact base.
|
- exact base.
|
||||||
- intro a. exact base.
|
- intro a. exact base.
|
||||||
- exact S1op.
|
- exact S1op.
|
||||||
- apply S1op_assoc.
|
- apply S1op_assoc.
|
||||||
- apply S1op_comm.
|
- apply S1op_comm.
|
||||||
- apply S1op_nl.
|
- apply S1op_nl.
|
||||||
- apply S1op_nr.
|
- apply S1op_nr.
|
||||||
- simpl. reflexivity.
|
- simpl. reflexivity.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma FSet_S_ap : (nl (@E A)) = (nr E) -> idpath = loop.
|
Lemma FSet_S_ap : (nl (@E A)) = (nr E) -> idpath = loop.
|
||||||
Proof.
|
Proof.
|
||||||
intros H.
|
intros H.
|
||||||
enough (ap FSet_to_S (nl E) = ap FSet_to_S (nr E)) as H'.
|
enough (ap FSet_to_S (nl E) = ap FSet_to_S (nr E)) as H'.
|
||||||
- rewrite FSet_rec_beta_nl in H'.
|
- rewrite FSet_rec_beta_nl in H'.
|
||||||
rewrite FSet_rec_beta_nr in H'.
|
rewrite FSet_rec_beta_nr in H'.
|
||||||
simpl in H'. unfold S1op_nr in H'.
|
simpl in H'. unfold S1op_nr in H'.
|
||||||
exact H'^.
|
exact H'^.
|
||||||
- f_ap.
|
- f_ap.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma FSet_not_hset : IsHSet (FSet A) -> False.
|
Lemma FSet_not_hset : IsHSet (FSet A) -> False.
|
||||||
Proof.
|
Proof.
|
||||||
intros H.
|
intros H.
|
||||||
enough (idpath = loop).
|
enough (idpath = loop).
|
||||||
- assert (S1_encode _ idpath = S1_encode _ (loopexp loop (pos Int.one))) as H' by f_ap.
|
- assert (S1_encode _ idpath = S1_encode _ (loopexp loop (pos Int.one))) as H' by f_ap.
|
||||||
rewrite S1_encode_loopexp in H'. simpl in H'. symmetry in H'.
|
rewrite S1_encode_loopexp in H'. simpl in H'. symmetry in H'.
|
||||||
apply (pos_neq_zero H').
|
apply (pos_neq_zero H').
|
||||||
- apply FSet_S_ap.
|
- apply FSet_S_ap.
|
||||||
apply set_path2.
|
apply set_path2.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
End set_sphere.
|
End set_sphere.
|
||||||
|
|
|
||||||
|
|
@ -1,323 +1,116 @@
|
||||||
|
(* Definition of Finite Sets as via cons lists *)
|
||||||
Require Import HoTT HitTactics.
|
Require Import HoTT HitTactics.
|
||||||
Require Import representations.definition.
|
|
||||||
From fsets Require Import operations_decidable properties_decidable.
|
|
||||||
|
|
||||||
Module Export FSetC.
|
Module Export FSetC.
|
||||||
|
|
||||||
Section FSetC.
|
Section FSetC.
|
||||||
Variable A : Type.
|
Variable A : Type.
|
||||||
|
|
||||||
Private Inductive FSetC : Type :=
|
Private Inductive FSetC : Type :=
|
||||||
| Nil : FSetC
|
| Nil : FSetC
|
||||||
| Cns : A -> FSetC -> FSetC.
|
| Cns : A -> FSetC -> FSetC.
|
||||||
|
|
||||||
Infix ";;" := Cns (at level 8, right associativity).
|
Infix ";;" := Cns (at level 8, right associativity).
|
||||||
Notation "∅" := Nil.
|
Notation "∅" := Nil.
|
||||||
|
|
||||||
Axiom dupl : forall (a: A) (x: FSetC),
|
Axiom dupl : forall (a: A) (x: FSetC),
|
||||||
a ;; a ;; x = a ;; x.
|
a ;; a ;; x = a ;; x.
|
||||||
|
|
||||||
Axiom comm : forall (a b: A) (x: FSetC),
|
Axiom comm : forall (a b: A) (x: FSetC),
|
||||||
a ;; b ;; x = b ;; a ;; x.
|
a ;; b ;; x = b ;; a ;; x.
|
||||||
|
|
||||||
Axiom trunc : IsHSet FSetC.
|
Axiom trunc : IsHSet FSetC.
|
||||||
|
|
||||||
|
End FSetC.
|
||||||
|
|
||||||
|
Arguments Nil {_}.
|
||||||
|
Arguments Cns {_} _ _.
|
||||||
|
Arguments dupl {_} _ _.
|
||||||
|
Arguments comm {_} _ _ _.
|
||||||
|
|
||||||
|
Infix ";;" := Cns (at level 8, right associativity).
|
||||||
|
Notation "∅" := Nil.
|
||||||
|
|
||||||
|
Section FSetC_induction.
|
||||||
|
|
||||||
|
Variable A: Type.
|
||||||
|
Variable (P : FSetC A -> Type).
|
||||||
|
Variable (H : forall x : FSetC A, IsHSet (P x)).
|
||||||
|
Variable (eP : P ∅).
|
||||||
|
Variable (cnsP : forall (a:A) (x: FSetC A), P x -> P (a ;; x)).
|
||||||
|
Variable (duplP : forall (a: A) (x: FSetC A) (px : P x),
|
||||||
|
dupl a x # cnsP a (a;;x) (cnsP a x px) = cnsP a x px).
|
||||||
|
Variable (commP : forall (a b: A) (x: FSetC A) (px: P x),
|
||||||
|
comm a b x # cnsP a (b;;x) (cnsP b x px) =
|
||||||
|
cnsP b (a;;x) (cnsP a x px)).
|
||||||
|
|
||||||
|
(* Induction principle *)
|
||||||
|
Fixpoint FSetC_ind
|
||||||
|
(x : FSetC A)
|
||||||
|
{struct x}
|
||||||
|
: P x
|
||||||
|
:= (match x return _ -> _ -> _ -> P x with
|
||||||
|
| Nil => fun _ => fun _ => fun _ => eP
|
||||||
|
| a ;; y => fun _ => fun _ => fun _ => cnsP a y (FSetC_ind y)
|
||||||
|
end) H duplP commP.
|
||||||
|
|
||||||
|
|
||||||
|
Axiom FSetC_ind_beta_dupl : forall (a: A) (x : FSetC A),
|
||||||
|
apD FSetC_ind (dupl a x) = duplP a x (FSetC_ind x).
|
||||||
|
|
||||||
|
Axiom FSetC_ind_beta_comm : forall (a b: A) (x : FSetC A),
|
||||||
|
apD FSetC_ind (comm a b x) = commP a b x (FSetC_ind x).
|
||||||
|
|
||||||
|
End FSetC_induction.
|
||||||
|
|
||||||
|
Section FSetC_recursion.
|
||||||
|
|
||||||
|
Variable A: Type.
|
||||||
|
Variable (P: Type).
|
||||||
|
Variable (H: IsHSet P).
|
||||||
|
Variable (nil : P).
|
||||||
|
Variable (cns : A -> P -> P).
|
||||||
|
Variable (duplP : forall (a: A) (x: P), cns a (cns a x) = (cns a x)).
|
||||||
|
Variable (commP : forall (a b: A) (x: P), cns a (cns b x) = cns b (cns a x)).
|
||||||
|
|
||||||
|
(* Recursion principle *)
|
||||||
|
Definition FSetC_rec : FSetC A -> P.
|
||||||
|
Proof.
|
||||||
|
simple refine (FSetC_ind _ _ _ _ _ _ _ );
|
||||||
|
try (intros; simple refine ((transport_const _ _) @ _ )); cbn.
|
||||||
|
- apply nil.
|
||||||
|
- apply (fun a => fun _ => cns a).
|
||||||
|
- apply duplP.
|
||||||
|
- apply commP.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
Definition FSetC_rec_beta_dupl : forall (a: A) (x : FSetC A),
|
||||||
|
ap FSetC_rec (dupl a x) = duplP a (FSetC_rec x).
|
||||||
|
Proof.
|
||||||
|
intros.
|
||||||
|
eapply (cancelL (transport_const (dupl a x) _)).
|
||||||
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
|
apply FSetC_ind_beta_dupl.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Definition FSetC_rec_beta_comm : forall (a b: A) (x : FSetC A),
|
||||||
|
ap FSetC_rec (comm a b x) = commP a b (FSetC_rec x).
|
||||||
|
Proof.
|
||||||
|
intros.
|
||||||
|
eapply (cancelL (transport_const (comm a b x) _)).
|
||||||
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
|
apply FSetC_ind_beta_comm.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
End FSetC_recursion.
|
||||||
|
|
||||||
|
|
||||||
|
Instance FSetC_recursion A : HitRecursion (FSetC A) := {
|
||||||
|
indTy := _; recTy := _;
|
||||||
|
H_inductor := FSetC_ind A; H_recursor := FSetC_rec A }.
|
||||||
|
|
||||||
End FSetC.
|
End FSetC.
|
||||||
|
|
||||||
Arguments Nil {_}.
|
|
||||||
Arguments Cns {_} _ _.
|
|
||||||
Arguments dupl {_} _ _.
|
|
||||||
Arguments comm {_} _ _ _.
|
|
||||||
|
|
||||||
Infix ";;" := Cns (at level 8, right associativity).
|
Infix ";;" := Cns (at level 8, right associativity).
|
||||||
Notation "∅" := Nil.
|
Notation "∅" := Nil.
|
||||||
|
|
||||||
Section FSetC_induction.
|
|
||||||
|
|
||||||
Variable A: Type.
|
|
||||||
Variable (P : FSetC A -> Type).
|
|
||||||
Variable (H : forall x : FSetC A, IsHSet (P x)).
|
|
||||||
Variable (eP : P ∅).
|
|
||||||
Variable (cnsP : forall (a:A) (x: FSetC A), P x -> P (a ;; x)).
|
|
||||||
Variable (duplP : forall (a: A) (x: FSetC A) (px : P x),
|
|
||||||
dupl a x # cnsP a (a;;x) (cnsP a x px) = cnsP a x px).
|
|
||||||
Variable (commP : forall (a b: A) (x: FSetC A) (px: P x),
|
|
||||||
comm a b x # cnsP a (b;;x) (cnsP b x px) =
|
|
||||||
cnsP b (a;;x) (cnsP a x px)).
|
|
||||||
|
|
||||||
(* Induction principle *)
|
|
||||||
Fixpoint FSetC_ind
|
|
||||||
(x : FSetC A)
|
|
||||||
{struct x}
|
|
||||||
: P x
|
|
||||||
:= (match x return _ -> _ -> _ -> P x with
|
|
||||||
| Nil => fun _ => fun _ => fun _ => eP
|
|
||||||
| a ;; y => fun _ => fun _ => fun _ => cnsP a y (FSetC_ind y)
|
|
||||||
end) H duplP commP.
|
|
||||||
|
|
||||||
|
|
||||||
Axiom FSetC_ind_beta_dupl : forall (a: A) (x : FSetC A),
|
|
||||||
apD FSetC_ind (dupl a x) = duplP a x (FSetC_ind x).
|
|
||||||
|
|
||||||
Axiom FSetC_ind_beta_comm : forall (a b: A) (x : FSetC A),
|
|
||||||
apD FSetC_ind (comm a b x) = commP a b x (FSetC_ind x).
|
|
||||||
|
|
||||||
End FSetC_induction.
|
|
||||||
|
|
||||||
Section FSetC_recursion.
|
|
||||||
|
|
||||||
Variable A: Type.
|
|
||||||
Variable (P: Type).
|
|
||||||
Variable (H: IsHSet P).
|
|
||||||
Variable (nil : P).
|
|
||||||
Variable (cns : A -> P -> P).
|
|
||||||
Variable (duplP : forall (a: A) (x: P), cns a (cns a x) = (cns a x)).
|
|
||||||
Variable (commP : forall (a b: A) (x: P), cns a (cns b x) = cns b (cns a x)).
|
|
||||||
|
|
||||||
(* Recursion principle *)
|
|
||||||
Definition FSetC_rec : FSetC A -> P.
|
|
||||||
Proof.
|
|
||||||
simple refine (FSetC_ind _ _ _ _ _ _ _ );
|
|
||||||
try (intros; simple refine ((transport_const _ _) @ _ )); cbn.
|
|
||||||
- apply nil.
|
|
||||||
- apply (fun a => fun _ => cns a).
|
|
||||||
- apply duplP.
|
|
||||||
- apply commP.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
|
|
||||||
Definition FSetC_rec_beta_dupl : forall (a: A) (x : FSetC A),
|
|
||||||
ap FSetC_rec (dupl a x) = duplP a (FSetC_rec x).
|
|
||||||
Proof.
|
|
||||||
intros.
|
|
||||||
unfold FSet_rec.
|
|
||||||
eapply (cancelL (transport_const (dupl a x) _)).
|
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
|
||||||
apply FSetC_ind_beta_dupl.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Definition FSetC_rec_beta_comm : forall (a b: A) (x : FSetC A),
|
|
||||||
ap FSetC_rec (comm a b x) = commP a b (FSetC_rec x).
|
|
||||||
Proof.
|
|
||||||
intros.
|
|
||||||
unfold FSet_rec.
|
|
||||||
eapply (cancelL (transport_const (comm a b x) _)).
|
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
|
||||||
apply FSetC_ind_beta_comm.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
End FSetC_recursion.
|
|
||||||
|
|
||||||
|
|
||||||
Instance FSetC_recursion A : HitRecursion (FSetC A) := {
|
|
||||||
indTy := _; recTy := _;
|
|
||||||
H_inductor := FSetC_ind A; H_recursor := FSetC_rec A }.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Section Append.
|
|
||||||
|
|
||||||
Context {A : Type}.
|
|
||||||
Context {A_deceq : DecidablePaths A}.
|
|
||||||
|
|
||||||
Definition append (x y: FSetC A) : FSetC A.
|
|
||||||
hinduction x.
|
|
||||||
- apply y.
|
|
||||||
- apply Cns.
|
|
||||||
- apply dupl.
|
|
||||||
- apply comm.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma append_nl:
|
|
||||||
forall (x: FSetC A), append ∅ x = x.
|
|
||||||
Proof.
|
|
||||||
intro. reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma append_nr:
|
|
||||||
forall (x: FSetC A), append x ∅ = x.
|
|
||||||
Proof.
|
|
||||||
hinduction; try (intros; apply set_path2).
|
|
||||||
- reflexivity.
|
|
||||||
- intros. apply (ap (fun y => a ;; y) X).
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma append_assoc {H: Funext}:
|
|
||||||
forall (x y z: FSetC A), append x (append y z) = append (append x y) z.
|
|
||||||
Proof.
|
|
||||||
intro x; hinduction x; try (intros; apply set_path2).
|
|
||||||
- reflexivity.
|
|
||||||
- intros a x HR y z.
|
|
||||||
specialize (HR y z).
|
|
||||||
apply (ap (fun y => a ;; y) HR).
|
|
||||||
- intros. apply path_forall.
|
|
||||||
intro. apply path_forall.
|
|
||||||
intro. apply set_path2.
|
|
||||||
- intros. apply path_forall.
|
|
||||||
intro. apply path_forall.
|
|
||||||
intro. apply set_path2.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma aux: forall (a: A) (x: FSetC A),
|
|
||||||
a ;; x = append x (a ;; ∅).
|
|
||||||
Proof.
|
|
||||||
intro a. hinduction; try (intros; apply set_path2).
|
|
||||||
- reflexivity.
|
|
||||||
- intros b x HR. refine (_ @ _).
|
|
||||||
+ apply comm.
|
|
||||||
+ apply (ap (fun y => b ;; y) HR).
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma append_comm {H: Funext}:
|
|
||||||
forall (x1 x2: FSetC A), append x1 x2 = append x2 x1.
|
|
||||||
Proof.
|
|
||||||
intro x1.
|
|
||||||
hinduction x1; try (intros; apply set_path2).
|
|
||||||
- intros. symmetry. apply append_nr.
|
|
||||||
- intros a x1 HR x2.
|
|
||||||
etransitivity.
|
|
||||||
apply (ap (fun y => a;;y) (HR x2)).
|
|
||||||
transitivity (append (append x2 x1) (a;;∅)).
|
|
||||||
+ apply aux.
|
|
||||||
+ etransitivity.
|
|
||||||
* symmetry. apply append_assoc.
|
|
||||||
* simple refine (ap (fun y => append x2 y) (aux _ _)^).
|
|
||||||
- intros. apply path_forall.
|
|
||||||
intro. apply set_path2.
|
|
||||||
- intros. apply path_forall.
|
|
||||||
intro. apply set_path2.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
|
|
||||||
End Append.
|
|
||||||
|
|
||||||
|
|
||||||
Section Singleton.
|
|
||||||
|
|
||||||
Context {A : Type}.
|
|
||||||
Context {A_deceq : DecidablePaths A}.
|
|
||||||
|
|
||||||
Definition singleton (a:A) : FSetC A := a;;∅.
|
|
||||||
|
|
||||||
Lemma singleton_idem: forall (a: A),
|
|
||||||
append (singleton a) (singleton a) = singleton a.
|
|
||||||
Proof.
|
|
||||||
unfold singleton. intro. cbn. apply dupl.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
End Singleton.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Infix ";;" := Cns (at level 8, right associativity).
|
|
||||||
Notation "∅" := Nil.
|
|
||||||
|
|
||||||
End FSetC.
|
|
||||||
|
|
||||||
|
|
||||||
Section Iso.
|
|
||||||
|
|
||||||
Context {A : Type}.
|
|
||||||
Context {A_deceq : DecidablePaths A}.
|
|
||||||
Context {H : Funext}.
|
|
||||||
|
|
||||||
|
|
||||||
Definition FSetC_to_FSet: FSetC A -> FSet A.
|
|
||||||
Proof.
|
|
||||||
hrecursion.
|
|
||||||
- apply E.
|
|
||||||
- intros a x. apply (U (L a) x).
|
|
||||||
- intros. cbn.
|
|
||||||
etransitivity. apply assoc.
|
|
||||||
apply (ap (fun y => U y x)).
|
|
||||||
apply idem.
|
|
||||||
- intros. cbn.
|
|
||||||
etransitivity. apply assoc.
|
|
||||||
etransitivity. refine (ap (fun y => U y x) _ ).
|
|
||||||
apply FSet.comm.
|
|
||||||
symmetry.
|
|
||||||
apply assoc.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Definition FSet_to_FSetC: FSet A -> FSetC A :=
|
|
||||||
FSet_rec A (FSetC A) (trunc A) ∅ singleton append append_assoc
|
|
||||||
append_comm append_nl append_nr singleton_idem.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma append_union: forall (x y: FSetC A),
|
|
||||||
FSetC_to_FSet (append x y) = U (FSetC_to_FSet x) (FSetC_to_FSet y).
|
|
||||||
Proof.
|
|
||||||
intros x.
|
|
||||||
hrecursion x; try (intros; apply path_forall; intro; apply set_path2).
|
|
||||||
- intros. symmetry. apply nl.
|
|
||||||
- intros a x HR y. rewrite HR. apply assoc.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma repr_iso_id_l: forall (x: FSet A), FSetC_to_FSet (FSet_to_FSetC x) = x.
|
|
||||||
Proof.
|
|
||||||
hinduction; try (intros; apply set_path2).
|
|
||||||
- reflexivity.
|
|
||||||
- intro. apply nr.
|
|
||||||
- intros x y p q. rewrite append_union, p, q. reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma repr_iso_id_r: forall (x: FSetC A), FSet_to_FSetC (FSetC_to_FSet x) = x.
|
|
||||||
Proof.
|
|
||||||
hinduction; try (intros; apply set_path2).
|
|
||||||
- reflexivity.
|
|
||||||
- intros a x HR. rewrite HR. reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
|
|
||||||
Theorem repr_iso: FSet A <~> FSetC A.
|
|
||||||
Proof.
|
|
||||||
simple refine (@BuildEquiv (FSet A) (FSetC A) FSet_to_FSetC _ ).
|
|
||||||
apply isequiv_biinv.
|
|
||||||
unfold BiInv. split.
|
|
||||||
exists FSetC_to_FSet.
|
|
||||||
unfold Sect. apply repr_iso_id_l.
|
|
||||||
exists FSetC_to_FSet.
|
|
||||||
unfold Sect. apply repr_iso_id_r.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
End Iso.
|
|
||||||
|
|
||||||
Section Length.
|
|
||||||
|
|
||||||
Context {A : Type}.
|
|
||||||
Context {A_deceq : DecidablePaths A}.
|
|
||||||
Context `{Univalence}.
|
|
||||||
|
|
||||||
Opaque isIn_b.
|
|
||||||
Definition length (x: FSetC A) : nat.
|
|
||||||
Proof.
|
|
||||||
simple refine (FSetC_ind A _ _ _ _ _ _ x ); simpl.
|
|
||||||
- exact 0.
|
|
||||||
- intros a y n.
|
|
||||||
pose (y' := FSetC_to_FSet y).
|
|
||||||
exact (if isIn_b a y' then n else (S n)).
|
|
||||||
- intros. rewrite transport_const. cbn.
|
|
||||||
simplify_isIn. simpl. reflexivity.
|
|
||||||
- intros. rewrite transport_const. cbn.
|
|
||||||
simplify_isIn.
|
|
||||||
destruct (dec (a = b)) as [Hab | Hab].
|
|
||||||
+ rewrite Hab. simplify_isIn. simpl. reflexivity.
|
|
||||||
+ rewrite ?L_isIn_b_false; auto. simpl.
|
|
||||||
destruct (isIn_b a (FSetC_to_FSet x0)), (isIn_b b (FSetC_to_FSet x0)) ; reflexivity.
|
|
||||||
intro p. contradiction (Hab p^).
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Definition length_FSet (x: FSet A) := length (FSet_to_FSetC x).
|
|
||||||
|
|
||||||
Lemma length_singleton: forall (a: A), length_FSet (L a) = 1.
|
|
||||||
Proof.
|
|
||||||
intro a.
|
|
||||||
cbn. reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
End Length.
|
|
||||||
|
|
|
||||||
|
|
@ -3,190 +3,189 @@ Require Import HoTT.
|
||||||
Require Import HitTactics.
|
Require Import HitTactics.
|
||||||
|
|
||||||
Module Export FSet.
|
Module Export FSet.
|
||||||
|
Section FSet.
|
||||||
|
Variable A : Type.
|
||||||
|
|
||||||
Section FSet.
|
Private Inductive FSet : Type :=
|
||||||
Variable A : Type.
|
| E : FSet
|
||||||
|
| L : A -> FSet
|
||||||
|
| U : FSet -> FSet -> FSet.
|
||||||
|
|
||||||
Private Inductive FSet : Type :=
|
Notation "{| x |}" := (L x).
|
||||||
| E : FSet
|
Infix "∪" := U (at level 8, right associativity).
|
||||||
| L : A -> FSet
|
Notation "∅" := E.
|
||||||
| U : FSet -> FSet -> FSet.
|
|
||||||
|
|
||||||
Notation "{| x |}" := (L x).
|
Axiom assoc : forall (x y z : FSet ),
|
||||||
Infix "∪" := U (at level 8, right associativity).
|
x ∪ (y ∪ z) = (x ∪ y) ∪ z.
|
||||||
Notation "∅" := E.
|
|
||||||
|
|
||||||
Axiom assoc : forall (x y z : FSet ),
|
Axiom comm : forall (x y : FSet),
|
||||||
x ∪ (y ∪ z) = (x ∪ y) ∪ z.
|
x ∪ y = y ∪ x.
|
||||||
|
|
||||||
Axiom comm : forall (x y : FSet),
|
Axiom nl : forall (x : FSet),
|
||||||
x ∪ y = y ∪ x.
|
∅ ∪ x = x.
|
||||||
|
|
||||||
Axiom nl : forall (x : FSet),
|
Axiom nr : forall (x : FSet),
|
||||||
∅ ∪ x = x.
|
x ∪ ∅ = x.
|
||||||
|
|
||||||
Axiom nr : forall (x : FSet),
|
Axiom idem : forall (x : A),
|
||||||
x ∪ ∅ = x.
|
{| x |} ∪ {|x|} = {|x|}.
|
||||||
|
|
||||||
Axiom idem : forall (x : A),
|
Axiom trunc : IsHSet FSet.
|
||||||
{| x |} ∪ {|x|} = {|x|}.
|
|
||||||
|
|
||||||
Axiom trunc : IsHSet FSet.
|
End FSet.
|
||||||
|
|
||||||
End FSet.
|
Arguments E {_}.
|
||||||
|
Arguments U {_} _ _.
|
||||||
|
Arguments L {_} _.
|
||||||
|
Arguments assoc {_} _ _ _.
|
||||||
|
Arguments comm {_} _ _.
|
||||||
|
Arguments nl {_} _.
|
||||||
|
Arguments nr {_} _.
|
||||||
|
Arguments idem {_} _.
|
||||||
|
|
||||||
Arguments E {_}.
|
Section FSet_induction.
|
||||||
Arguments U {_} _ _.
|
Variable A: Type.
|
||||||
Arguments L {_} _.
|
Variable (P : FSet A -> Type).
|
||||||
Arguments assoc {_} _ _ _.
|
Variable (H : forall a : FSet A, IsHSet (P a)).
|
||||||
Arguments comm {_} _ _.
|
Variable (eP : P E).
|
||||||
Arguments nl {_} _.
|
Variable (lP : forall a: A, P (L a)).
|
||||||
Arguments nr {_} _.
|
Variable (uP : forall (x y: FSet A), P x -> P y -> P (U x y)).
|
||||||
Arguments idem {_} _.
|
Variable (assocP : forall (x y z : FSet A)
|
||||||
|
(px: P x) (py: P y) (pz: P z),
|
||||||
|
assoc x y z #
|
||||||
|
(uP x (U y z) px (uP y z py pz))
|
||||||
|
=
|
||||||
|
(uP (U x y) z (uP x y px py) pz)).
|
||||||
|
Variable (commP : forall (x y: FSet A) (px: P x) (py: P y),
|
||||||
|
comm x y #
|
||||||
|
uP x y px py = uP y x py px).
|
||||||
|
Variable (nlP : forall (x : FSet A) (px: P x),
|
||||||
|
nl x # uP E x eP px = px).
|
||||||
|
Variable (nrP : forall (x : FSet A) (px: P x),
|
||||||
|
nr x # uP x E px eP = px).
|
||||||
|
Variable (idemP : forall (x : A),
|
||||||
|
idem x # uP (L x) (L x) (lP x) (lP x) = lP x).
|
||||||
|
|
||||||
Section FSet_induction.
|
(* Induction principle *)
|
||||||
Variable A: Type.
|
Fixpoint FSet_ind
|
||||||
Variable (P : FSet A -> Type).
|
(x : FSet A)
|
||||||
Variable (H : forall a : FSet A, IsHSet (P a)).
|
{struct x}
|
||||||
Variable (eP : P E).
|
: P x
|
||||||
Variable (lP : forall a: A, P (L a)).
|
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
|
||||||
Variable (uP : forall (x y: FSet A), P x -> P y -> P (U x y)).
|
| E => fun _ _ _ _ _ _ => eP
|
||||||
Variable (assocP : forall (x y z : FSet A)
|
| L a => fun _ _ _ _ _ _ => lP a
|
||||||
(px: P x) (py: P y) (pz: P z),
|
| U y z => fun _ _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z)
|
||||||
assoc x y z #
|
end) H assocP commP nlP nrP idemP.
|
||||||
(uP x (U y z) px (uP y z py pz))
|
|
||||||
=
|
|
||||||
(uP (U x y) z (uP x y px py) pz)).
|
|
||||||
Variable (commP : forall (x y: FSet A) (px: P x) (py: P y),
|
|
||||||
comm x y #
|
|
||||||
uP x y px py = uP y x py px).
|
|
||||||
Variable (nlP : forall (x : FSet A) (px: P x),
|
|
||||||
nl x # uP E x eP px = px).
|
|
||||||
Variable (nrP : forall (x : FSet A) (px: P x),
|
|
||||||
nr x # uP x E px eP = px).
|
|
||||||
Variable (idemP : forall (x : A),
|
|
||||||
idem x # uP (L x) (L x) (lP x) (lP x) = lP x).
|
|
||||||
|
|
||||||
(* Induction principle *)
|
Axiom FSet_ind_beta_assoc : forall (x y z : FSet A),
|
||||||
Fixpoint FSet_ind
|
apD FSet_ind (assoc x y z) =
|
||||||
(x : FSet A)
|
(assocP x y z (FSet_ind x) (FSet_ind y) (FSet_ind z)).
|
||||||
{struct x}
|
|
||||||
: P x
|
|
||||||
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
|
|
||||||
| E => fun _ _ _ _ _ _ => eP
|
|
||||||
| L a => fun _ _ _ _ _ _ => lP a
|
|
||||||
| U y z => fun _ _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z)
|
|
||||||
end) H assocP commP nlP nrP idemP.
|
|
||||||
|
|
||||||
|
Axiom FSet_ind_beta_comm : forall (x y : FSet A),
|
||||||
|
apD FSet_ind (comm x y) = (commP x y (FSet_ind x) (FSet_ind y)).
|
||||||
|
|
||||||
Axiom FSet_ind_beta_assoc : forall (x y z : FSet A),
|
Axiom FSet_ind_beta_nl : forall (x : FSet A),
|
||||||
apD FSet_ind (assoc x y z) =
|
apD FSet_ind (nl x) = (nlP x (FSet_ind x)).
|
||||||
(assocP x y z (FSet_ind x) (FSet_ind y) (FSet_ind z)).
|
|
||||||
|
|
||||||
Axiom FSet_ind_beta_comm : forall (x y : FSet A),
|
Axiom FSet_ind_beta_nr : forall (x : FSet A),
|
||||||
apD FSet_ind (comm x y) = (commP x y (FSet_ind x) (FSet_ind y)).
|
apD FSet_ind (nr x) = (nrP x (FSet_ind x)).
|
||||||
|
|
||||||
Axiom FSet_ind_beta_nl : forall (x : FSet A),
|
Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x.
|
||||||
apD FSet_ind (nl x) = (nlP x (FSet_ind x)).
|
End FSet_induction.
|
||||||
|
|
||||||
Axiom FSet_ind_beta_nr : forall (x : FSet A),
|
Section FSet_recursion.
|
||||||
apD FSet_ind (nr x) = (nrP x (FSet_ind x)).
|
|
||||||
|
|
||||||
Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x.
|
Variable A : Type.
|
||||||
End FSet_induction.
|
Variable P : Type.
|
||||||
|
Variable H: IsHSet P.
|
||||||
|
Variable e : P.
|
||||||
|
Variable l : A -> P.
|
||||||
|
Variable u : P -> P -> P.
|
||||||
|
Variable assocP : forall (x y z : P), u x (u y z) = u (u x y) z.
|
||||||
|
Variable commP : forall (x y : P), u x y = u y x.
|
||||||
|
Variable nlP : forall (x : P), u e x = x.
|
||||||
|
Variable nrP : forall (x : P), u x e = x.
|
||||||
|
Variable idemP : forall (x : A), u (l x) (l x) = l x.
|
||||||
|
|
||||||
Section FSet_recursion.
|
Definition FSet_rec : FSet A -> P.
|
||||||
|
Proof.
|
||||||
|
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _)
|
||||||
|
; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn.
|
||||||
|
- apply e.
|
||||||
|
- apply l.
|
||||||
|
- intros x y ; apply u.
|
||||||
|
- apply assocP.
|
||||||
|
- apply commP.
|
||||||
|
- apply nlP.
|
||||||
|
- apply nrP.
|
||||||
|
- apply idemP.
|
||||||
|
Defined.
|
||||||
|
|
||||||
Variable A : Type.
|
Definition FSet_rec_beta_assoc : forall (x y z : FSet A),
|
||||||
Variable P : Type.
|
ap FSet_rec (assoc x y z)
|
||||||
Variable H: IsHSet P.
|
=
|
||||||
Variable e : P.
|
assocP (FSet_rec x) (FSet_rec y) (FSet_rec z).
|
||||||
Variable l : A -> P.
|
Proof.
|
||||||
Variable u : P -> P -> P.
|
intros.
|
||||||
Variable assocP : forall (x y z : P), u x (u y z) = u (u x y) z.
|
unfold FSet_rec.
|
||||||
Variable commP : forall (x y : P), u x y = u y x.
|
eapply (cancelL (transport_const (assoc x y z) _)).
|
||||||
Variable nlP : forall (x : P), u e x = x.
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
Variable nrP : forall (x : P), u x e = x.
|
apply FSet_ind_beta_assoc.
|
||||||
Variable idemP : forall (x : A), u (l x) (l x) = l x.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec : FSet A -> P.
|
Definition FSet_rec_beta_comm : forall (x y : FSet A),
|
||||||
Proof.
|
ap FSet_rec (comm x y)
|
||||||
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn.
|
=
|
||||||
- apply e.
|
commP (FSet_rec x) (FSet_rec y).
|
||||||
- apply l.
|
Proof.
|
||||||
- intros x y ; apply u.
|
intros.
|
||||||
- apply assocP.
|
unfold FSet_rec.
|
||||||
- apply commP.
|
eapply (cancelL (transport_const (comm x y) _)).
|
||||||
- apply nlP.
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
- apply nrP.
|
apply FSet_ind_beta_comm.
|
||||||
- apply idemP.
|
Defined.
|
||||||
Defined.
|
|
||||||
|
|
||||||
Definition FSet_rec_beta_assoc : forall (x y z : FSet A),
|
Definition FSet_rec_beta_nl : forall (x : FSet A),
|
||||||
ap FSet_rec (assoc x y z)
|
ap FSet_rec (nl x)
|
||||||
=
|
=
|
||||||
assocP (FSet_rec x) (FSet_rec y) (FSet_rec z).
|
nlP (FSet_rec x).
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
unfold FSet_rec.
|
unfold FSet_rec.
|
||||||
eapply (cancelL (transport_const (assoc x y z) _)).
|
eapply (cancelL (transport_const (nl x) _)).
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
apply FSet_ind_beta_assoc.
|
apply FSet_ind_beta_nl.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec_beta_comm : forall (x y : FSet A),
|
Definition FSet_rec_beta_nr : forall (x : FSet A),
|
||||||
ap FSet_rec (comm x y)
|
ap FSet_rec (nr x)
|
||||||
=
|
=
|
||||||
commP (FSet_rec x) (FSet_rec y).
|
nrP (FSet_rec x).
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
unfold FSet_rec.
|
unfold FSet_rec.
|
||||||
eapply (cancelL (transport_const (comm x y) _)).
|
eapply (cancelL (transport_const (nr x) _)).
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
apply FSet_ind_beta_comm.
|
apply FSet_ind_beta_nr.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec_beta_nl : forall (x : FSet A),
|
Definition FSet_rec_beta_idem : forall (a : A),
|
||||||
ap FSet_rec (nl x)
|
ap FSet_rec (idem a)
|
||||||
=
|
=
|
||||||
nlP (FSet_rec x).
|
idemP a.
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
unfold FSet_rec.
|
unfold FSet_rec.
|
||||||
eapply (cancelL (transport_const (nl x) _)).
|
eapply (cancelL (transport_const (idem a) _)).
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
simple refine ((apD_const _ _)^ @ _).
|
||||||
apply FSet_ind_beta_nl.
|
apply FSet_ind_beta_idem.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_rec_beta_nr : forall (x : FSet A),
|
End FSet_recursion.
|
||||||
ap FSet_rec (nr x)
|
|
||||||
=
|
|
||||||
nrP (FSet_rec x).
|
|
||||||
Proof.
|
|
||||||
intros.
|
|
||||||
unfold FSet_rec.
|
|
||||||
eapply (cancelL (transport_const (nr x) _)).
|
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
|
||||||
apply FSet_ind_beta_nr.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Definition FSet_rec_beta_idem : forall (a : A),
|
Instance FSet_recursion A : HitRecursion (FSet A) := {
|
||||||
ap FSet_rec (idem a)
|
indTy := _; recTy := _;
|
||||||
=
|
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
|
||||||
idemP a.
|
|
||||||
Proof.
|
|
||||||
intros.
|
|
||||||
unfold FSet_rec.
|
|
||||||
eapply (cancelL (transport_const (idem a) _)).
|
|
||||||
simple refine ((apD_const _ _)^ @ _).
|
|
||||||
apply FSet_ind_beta_idem.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
End FSet_recursion.
|
|
||||||
|
|
||||||
Instance FSet_recursion A : HitRecursion (FSet A) := {
|
|
||||||
indTy := _; recTy := _;
|
|
||||||
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
|
|
||||||
|
|
||||||
End FSet.
|
End FSet.
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue