dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

Replace the canonical structures mechanism for recursion with type classes 

See changes in HitTactics.v
This commit is contained in:
Dan Frumin 2017-05-22 21:06:13 +02:00
parent 5e594d10f0
commit f23d4aeacb
3 changed files with 131 additions and 169 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

139
FinSets.v
View File

@ -319,10 +319,9 @@ Axiom FSet_ind_beta_idem : forall
End FSet.
(* TODO: add an induction principle *)
Definition FSetCL A : HitRec.class (FSet A) _ _ :=
HitRec.Class (FSet A) (fun x P H e l u aP cP lP rP iP => FSet_rec A P H e l u aP cP lP rP iP x) (fun x P H e l u aP cP lP rP iP => FSet_ind A P H e l u aP cP lP rP iP x).
Canonical Structure FSetTy A : HitRec.type := HitRec.Pack _ _ _ (FSetCL A).
Instance FSet_recursion A : HitRecursion (FSet A) := {
indTy := _; recTy := _;
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
Arguments E {_}.
Arguments U {_} _ _.
@ -332,28 +331,45 @@ End FinSet.
Section functions.
Parameter A : Type.
Parameter eq : A -> A -> Bool.
Parameter eq_refl: forall a:A, eq a a = true.
Parameter A_eqdec : forall (x y : A), Decidable (x = y).
Definition deceq (x y : A) :=
if dec (x = y) then true else false.
Definition isIn : A -> FSet A -> Bool.
Proof.
intros a X.
hrecursion X.
intros a.
hrecursion.
- exact false.
- intro a'. apply (eq a a').
- intro a'. apply (deceq a a').
- apply orb.
- intros x y z. compute. destruct x; reflexivity.
- intros x y. compute. destruct x, y; reflexivity.
- intros x. compute. reflexivity.
- intros x. compute. destruct x; reflexivity.
- intros a'. compute. destruct (eq a a'); reflexivity.
- intros a'. compute. destruct (A_eqdec a a'); reflexivity.
Defined.
Lemma isIn_eq a b : isIn a (L b) = true -> a = b.
Proof. cbv.
destruct (A_eqdec a b). intro. apply p.
intro X.
pose (false_ne_true X). contradiction.
Defined.
Lemma isIn_empt_false a : isIn a E = true -> Empty.
Proof.
cbv. intro X.
pose (false_ne_true X). contradiction.
Defined.
Lemma isIn_union a X Y : isIn a (U X Y) = orb (isIn a X) (isIn a Y).
Proof. reflexivity. Qed.
Definition comprehension :
(A -> Bool) -> FSet A -> FSet A.
Proof.
intros P X.
hrecursion X.
intros P.
hrecursion.
- apply E.
- intro a.
refine (if (P a) then L a else E).
@ -367,29 +383,40 @@ hrecursion X.
+ apply idem.
+ apply nl.
Defined.
Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E.
Proof.
hrecursion Y; try (intros; apply set_path2).
- cbn. reflexivity.
- cbn. reflexivity.
- intros x y IHa IHb.
cbn.
rewrite IHa.
rewrite IHb.
rewrite nl.
reflexivity.
Defined.
Require Import FunextAxiom.
Lemma comprehension_idem:
forall (X:FSet A), forall Y, comprehension (fun x => isIn x (U X Y)) X = X.
Proof.
simple refine (FSet_ind _ _ _ _ _ _ _ _ _ _ _); simpl.
hinduction; try (intros; apply set_path2).
- intro Y. cbv. reflexivity.
- intros a Y. unfold comprehension. unfold HitRec.hrecursion. simpl.
enough (isIn a (U (L a) Y) = true).
+ rewrite X. reflexivity.
+ unfold isIn. unfold HitRec.hrecursion. simpl.
rewrite eq_refl. auto.
- intros a Y. cbn.
unfold deceq;
destruct (dec (a = a)); simpl.
+ reflexivity.
+ contradiction n. reflexivity.
- intros X1 X2 IH1 IH2 Y.
unfold comprehension. unfold HitRec.hrecursion. simpl.
rewrite <- (assoc _ X1 X2 Y).
cbn -[isIn].
f_ap.
+ apply (IH1 (U X2 Y)).
+ rewrite (assoc _ X1 X2 Y).
rewrite (comm _ X1 X2).
+ rewrite <- assoc. apply (IH1 (U X2 Y)).
+ rewrite (comm _ X1 X2).
rewrite <- (assoc _ X2 X1 Y).
apply (IH2 (U X1 Y)).
Admitted.
Definition intersection :
FSet A -> FSet A -> FSet A.
Proof.
@ -411,68 +438,6 @@ hrecursion x.
destruct (isIn a y); reflexivity.
Defined.
Definition subset' (x : FSet A) (y : FSet A) : Bool.
Proof.
refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
Unshelve.
Focus 6.
apply x.
Focus 6.
apply true.
Focus 6.
intro a.
apply (isIn a y).
Focus 6.
intro b.
intro b'.
apply (andb b b').
Focus 1.
intros.
compute.
destruct x0.
destruct y0.
reflexivity.
reflexivity.
reflexivity.
Focus 1.
intros.
compute.
destruct x0.
destruct y0.
reflexivity.
reflexivity.
destruct y0.
reflexivity.
reflexivity.
Focus 1.
intros.
compute.
reflexivity.
Focus 1.
intros.
compute.
destruct x0.
reflexivity.
reflexivity.
intros.
destruct (isIn x0 y).
compute.
reflexivity.
compute.
reflexivity.
Defined.
(* TODO: subset = subset' *)
Definition equal_set (x : FSet A) (y : FSet A) : Bool
:= andb (subset x y) (subset y x).

143
HitTactics.v
View File

@ -1,86 +1,85 @@
Module HitRec.
Record class (H : Type) (* The HIT type itself *)
(indTy : H -> Type) (* The type of the induciton principle *)
(recTy : H -> Type) (* The type of the recursion principle *)
:= Class {
H_recursor : forall (x : H), recTy x;
H_inductor : forall (x : H), indTy x }.
Structure type := Pack { obj : Type ; ind : obj -> Type ; rec : obj -> Type ; class_of : class obj ind rec }.
Definition hrecursion (e : type) : forall x, rec e x :=
let 'Pack _ _ _ (Class r _) := e
in r.
Definition hinduction (e : type) : forall x, ind e x :=
let 'Pack _ _ _ (Class _ i) := e
in i.
Arguments hrecursion {e} x : simpl never.
Arguments hinduction {e} x : simpl never.
Arguments Class H {indTy recTy} H_recursor H_inductor.
End HitRec.
Class HitRecursion (H : Type) := {
indTy : Type;
recTy : Type;
H_inductor : indTy;
H_recursor : recTy
}.
Ltac hrecursion_ target :=
generalize dependent target;
match goal with
| [ |- _ -> ?P ] => intro target;
match type of (HitRec.hrecursion target) with
Definition hrecursion (H : Type) {HR : HitRecursion H} : @recTy H HR :=
@H_recursor H HR.
Definition hinduction (H : Type) {HR : HitRecursion H} : @indTy H HR :=
@H_inductor H HR.
Ltac hrecursion_ :=
lazymatch goal with
| [ |- ?T -> ?P ] =>
let hrec1 := eval cbv[hrecursion H_recursor] in (hrecursion T) in
let hrec := eval simpl in hrec1 in
match type of hrec with
| ?Q =>
match (eval simpl in Q) with
| forall Y, Y =>
simple refine (HitRec.hrecursion target P)
| forall Y _, Y =>
simple refine (HitRec.hrecursion target P _)
| forall Y _ _, Y =>
simple refine (HitRec.hrecursion target P _ _)
| forall Y _ _ _, Y =>
simple refine (HitRec.hrecursion target P _ _ _)
| forall Y _ _ _ _, Y =>
simple refine (HitRec.hrecursion target P _ _ _ _)
| forall Y _ _ _ _ _, Y =>
simple refine (HitRec.hrecursion target P _ _ _ _ _)
| forall Y _ _ _ _ _ _, Y =>
simple refine (HitRec.hrecursion target P _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _, Y =>
simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _, Y =>
simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _ _, Y =>
simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _ _ _, Y =>
simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _ _ _)
| forall Y, T -> Y =>
simple refine (hrec P)
| forall Y _, T -> Y =>
simple refine (hrec P _)
| forall Y _ _, T -> Y =>
simple refine (hrec P _ _)
| forall Y _ _ _, T -> Y =>
simple refine (hrec P _ _ _)
| forall Y _ _ _ _, T -> Y =>
simple refine (hrec P _ _ _ _)
| forall Y _ _ _ _ _, T -> Y =>
simple refine (hrec P _ _ _ _ _)
| forall Y _ _ _ _ _ _, T -> Y =>
simple refine (hrec P _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _, T -> Y =>
simple refine (hrec P _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _, T -> Y =>
simple refine (hrec P _ _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _ _, T -> Y =>
simple refine (hrec P _ _ _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _ _ _, T -> Y =>
simple refine (hrec P _ _ _ _ _ _ _ _ _ _)
| _ => fail "Cannot handle the recursion principle (too many parameters?) :("
end
end
| [ |- forall target, ?P] => intro target;
match type of (HitRec.hinduction target) with
| [ |- forall (target:?T), ?P] =>
let hind1 := eval cbv[hinduction H_inductor] in (hinduction T) in
let hind := eval simpl in hind1 in
match type of hind with
| ?Q =>
match (eval simpl in Q) with
| forall Y , Y target =>
simple refine (HitRec.hinduction target (fun target => P) _)
| forall Y _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _)
| forall Y _ _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _ _)
| forall Y _ _ _, Y target =>
let hrec:=(eval hnf in (HitRec.hinduction target)) in
simple refine (hrec (fun target => P) _ _ _)
| forall Y _ _ _ _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _ _ _ _)
| forall Y _ _ _ _ _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _)
| forall Y _ _ _ _ _ _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _ _, Y target =>
simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _ _ _)
| forall Y , (forall x, Y x) =>
simple refine (hind (fun target => P) _)
| forall Y _, (forall x, Y x) =>
simple refine (hind (fun target => P) _)
| forall Y _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _)
| forall Y _ _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _ _)
| forall Y _ _ _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _ _ _)
| forall Y _ _ _ _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _ _ _ _)
| forall Y _ _ _ _ _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _ _ _ _ _ _ _)
| forall Y _ _ _ _ _ _ _ _ _, (forall x, Y x) =>
simple refine (hind (fun target => P) _ _ _ _ _ _ _ _ _)
| _ => fail "Cannot handle the induction principle (too many parameters?) :("
end
end
(*| _ => fail "I am sorry, but something went wrong!"*)
end.
Ltac hrecursion x := hrecursion_ x; simpl; try (clear x).
Ltac hinduction x := hrecursion x.
Tactic Notation "hrecursion" := hrecursion_; simpl.
Tactic Notation "hrecursion" ident(x) := revert x; hrecursion.
Tactic Notation "hinduction" := hrecursion_; simpl.
Tactic Notation "hinduction" ident(x) := revert x; hrecursion.

18
Mod2.v
View File

@ -1,6 +1,6 @@
Require Export HoTT.
Require Import HitTactics.
Module Export modulo.
Private Inductive Mod2 : Type0 :=
@ -51,10 +51,10 @@ Axiom Mod2_rec_beta_mod : forall
(mod' : a = s (s a))
, ap (Mod2_rec P a s mod') mod = mod'.
Definition Mod2CL : HitRec.class Mod2 _ _ :=
HitRec.Class Mod2 (fun x P a s p => Mod2_rec P a s p x) (fun x P a s p => Mod2_ind P a s p x).
Canonical Structure Mod2ty : HitRec.type := HitRec.Pack Mod2 _ _ Mod2CL.
Instance: HitRecursion Mod2 := {
indTy := _; recTy := _;
H_inductor := Mod2_ind;
H_recursor := Mod2_rec }.
End modulo.
@ -62,7 +62,7 @@ End modulo.
Theorem modulo2 : forall n : Mod2, n = succ(succ n).
Proof.
intro n.
hrecursion n.
hinduction n.
- apply mod.
- intros n p.
apply (ap succ p).
@ -75,8 +75,7 @@ Defined.
Definition negate : Mod2 -> Mod2.
Proof.
intro x.
hrecursion x.
hrecursion.
- apply Z.
- intros. apply (succ H).
- simpl. apply mod.
@ -137,8 +136,7 @@ hinduction n.
rewrite ap_compose.
enough (ap Mod2_to_Bool mod = idpath).
+ rewrite X. hott_simpl.
+ unfold Mod2_to_Bool. unfold HitRec.hrecursion. simpl.
apply (Mod2_rec_beta_mod Bool false negb 1).
+ apply (Mod2_rec_beta_mod Bool false negb 1).
Defined.
Theorem adj :