Skip to content

Commit e5e5831

Browse files
gmalechagmalecha
committed
building on 8.6
1 parent d8d0bb3 commit e5e5831

File tree

11 files changed

+164
-150
lines changed

11 files changed

+164
-150
lines changed

‎theories/Data/Fin.v‎

Lines changed: 38 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
(** Numbers up to @n@ **)
12
Require Coq.Lists.List.
23
Require Import ExtLib.Core.RelDec.
34
Require Import ExtLib.Tactics.EqDep.
@@ -7,6 +8,9 @@ Set Implicit Arguments.
78
Set Strict Implicit.
89
Set Asymmetric Patterns.
910

11+
(** `fin n` corresponds to "naturals less than `n`",
12+
** i.e. a finite set of size n
13+
**)
1014
Inductive fin : nat -> Type :=
1115
| F0 : forall {n}, fin (S n)
1216
| FS : forall {n}, fin n -> fin (S n).
@@ -39,26 +43,26 @@ Qed.
3943

4044
Definition fin0_elim (f : fin 0) : forall T, T :=
4145
match f in fin n return match n with
42-
| 0 => forall T, T
43-
| _ => unit
46+
| 0 => forall T, T
47+
| _ => unit
4448
end with
45-
| F0 _ => tt
46-
| FS _ _ => tt
49+
| F0 _ => tt
50+
| FS _ _ => tt
4751
end.
4852

4953
Fixpoint pf_lt (n m : nat) : Prop :=
5054
match n , m with
51-
| 0 , S _ => True
52-
| S n , S m => pf_lt n m
53-
| _ , _ => False
55+
| 0 , S _ => True
56+
| S n , S m => pf_lt n m
57+
| _ , _ => False
5458
end.
5559

5660
Fixpoint make (m n : nat) {struct m} : pf_lt n m -> fin m :=
5761
match n as n , m as m return pf_lt n m -> fin m with
58-
| 0 , 0 => @False_rect _
59-
| 0 , S n => fun _ => F0
60-
| S n , 0 => @False_rect _
61-
| S n , S m => fun pf => FS (make m n pf)
62+
| 0 , 0 => @False_rect _
63+
| 0 , S n => fun _ => F0
64+
| S n , 0 => @False_rect _
65+
| S n , S m => fun pf => FS (make m n pf)
6266
end.
6367

6468
Notation "'##' n" := (@make _ n I) (at level 0).
@@ -71,41 +75,34 @@ Defined.
7175

7276
Fixpoint fin_eq_dec {n} (x : fin n) {struct x} : fin n -> bool :=
7377
match x in fin n' return fin n' -> bool with
74-
| F0 _ => fun y => match y with
75-
| F0 _ => true
76-
| _ => false
77-
end
78-
| FS n' x' => fun y : fin (S n') =>
79-
match y in fin n'' return (match n'' with
80-
| 0 => unit
81-
| S n'' => fin n''
82-
end -> bool) -> bool with
83-
| F0 _ => fun _ => false
84-
| FS _ y' => fun f => f y'
85-
end (fun y => fin_eq_dec x' y)
86-
end.
78+
| F0 _ => fun y => match y with
79+
| F0 _ => true
80+
| _ => false
81+
end
82+
| FS n' x' => fun y : fin (S n') =>
83+
match y in fin n'' return (match n'' with
84+
| 0 => unit
85+
| S n'' => fin n''
86+
end -> bool) -> bool with
87+
| F0 _ => fun _ => false
88+
| FS _ y' => fun f => f y'
89+
end (fun y => fin_eq_dec x' y)
90+
end.
8791

8892
Global Instance RelDec_fin_eq (n : nat) : RelDec (@eq (fin n)) :=
8993
{ rel_dec := fin_eq_dec }.
9094

9195
Global Instance RelDec_Correct_fin_eq (n : nat)
92-
: RelDec_Correct (RelDec_fin_eq n).
96+
: RelDec_Correct (RelDec_fin_eq n).
9397
Proof.
9498
constructor.
95-
induction x. simpl.
96-
intro. destruct (fin_case y) ; subst.
97-
intuition.
98-
destruct H ; subst.
99-
intuition ; try congruence.
100-
inversion H.
101-
intro ; destruct (fin_case y) ; subst ; simpl.
102-
intuition ; try congruence.
103-
inversion H.
104-
destruct H ; subst.
105-
split ; intro.
106-
f_equal ; eauto.
107-
eapply IHx.
108-
eapply H.
109-
inv_all ; subst.
110-
apply IHx. reflexivity.
99+
induction x.
100+
{ intro. destruct (fin_case y) ; subst.
101+
{ split; reflexivity. }
102+
{ destruct H. subst. simpl. split; congruence. } }
103+
{ intro; destruct (fin_case y) ; subst ; simpl.
104+
{ split; congruence. }
105+
{ destruct H. subst. simpl. split.
106+
{ intro; f_equal. eapply IHx. assumption. }
107+
{ intro. inv_all. apply IHx in H. assumption. } } }
111108
Qed.

‎theories/Data/HList.v‎

Lines changed: 44 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -302,43 +302,43 @@ Section hlist.
302302
| hlist_eqv_nil => I
303303
| hlist_eqv_cons l ls x y h1 h2 pf1 pf2 => _
304304
end IHx).
305-
simpl.
305+
simpl in *.
306306
subst. intros.
307-
f_equal. apply H0. assumption. }
307+
f_equal. tauto. }
308308
{ intros; subst. constructor; auto.
309309
reflexivity. } }
310310
Qed.
311311

312312
Fixpoint hlist_get ls a (m : member a ls) : hlist ls -> F a :=
313313
match m in member _ ls return hlist ls -> F a with
314-
| MZ _ => hlist_hd
315-
| MN _ _ r => fun hl => hlist_get r (hlist_tl hl)
314+
| MZ _ => hlist_hd
315+
| MN _ _ r => fun hl => hlist_get r (hlist_tl hl)
316316
end.
317317

318318
Fixpoint hlist_nth_error {ls} (hs : hlist ls) (n : nat)
319-
: option (match nth_error ls n with
320-
| None => unit
321-
| Some x => F x
322-
end) :=
323-
match hs in hlist ls return option (match nth_error ls n with
324-
| None => unit
325-
| Some x => F x
326-
end)
319+
: option match nth_error ls n with
320+
| None => unit
321+
| Some x => F x
322+
end :=
323+
match hs in hlist ls return option match nth_error ls n with
324+
| None => unit
325+
| Some x => F x
326+
end
327+
with
328+
| Hnil => None
329+
| Hcons l ls h hs =>
330+
match n as n return option match nth_error (l :: ls) n with
331+
| None => unit
332+
| Some x => F x
333+
end
327334
with
328-
| Hnil => None
329-
| Hcons l ls h hs =>
330-
match n as n return option (match nth_error (l :: ls) n with
331-
| None => unit
332-
| Some x => F x
333-
end)
334-
with
335-
| 0 => Some h
336-
| S n => hlist_nth_error hs n
337-
end
335+
| 0 => Some h
336+
| S n => hlist_nth_error hs n
337+
end
338338
end.
339339

340-
Polymorphic Fixpoint hlist_nth ls (h : hlist ls) (n : nat) :
341-
match nth_error ls n return Type with
340+
Polymorphic Fixpoint hlist_nth ls (h : hlist ls) (n : nat)
341+
: match nth_error ls n return Type with
342342
| None => unit
343343
| Some t => F t
344344
end :=
@@ -584,9 +584,9 @@ Section hlist.
584584
match goal with
585585
| |- context [ match ?X with _ => _ end ] =>
586586
remember X
587-
end. destruct p. simpl.
587+
end. destruct p. simpl in *.
588588
change h0 with (fst (h0, h1)).
589-
f_equal.
589+
f_equal. assumption.
590590
Qed.
591591

592592
Lemma hlist_tl_snd_hlist_split
@@ -604,29 +604,29 @@ Section hlist.
604604
rewrite Heqp. reflexivity.
605605
Qed.
606606

607-
Polymorphic Fixpoint nth_error_get_hlist_nth (ls : list iT) (n : nat) {struct ls} :
608-
option {t : iT & hlist ls -> F t} :=
607+
Polymorphic Fixpoint nth_error_get_hlist_nth (ls : list iT) (n : nat) {struct ls}
608+
: option {t : iT & hlist ls -> F t} :=
609609
match
610610
ls as ls0
611611
return option {t : iT & hlist ls0 -> F t}
612612
with
613-
| nil => None
614-
| l :: ls0 =>
615-
match
616-
n as n0
617-
return option {t : iT & hlist (l :: ls0) -> F t}
618-
with
619-
| 0 =>
620-
Some (@existT _ (fun t => hlist (l :: ls0) -> F t)
621-
l (@hlist_hd _ _))
622-
| S n0 =>
623-
match nth_error_get_hlist_nth ls0 n0 with
624-
| Some (existT x f) =>
625-
Some (@existT _ (fun t => hlist _ -> F t)
626-
x (fun h : hlist (l :: ls0) => f (hlist_tl h)))
627-
| None => None
628-
end
613+
| nil => None
614+
| l :: ls0 =>
615+
match
616+
n as n0
617+
return option {t : iT & hlist (l :: ls0) -> F t}
618+
with
619+
| 0 =>
620+
Some (@existT _ (fun t => hlist (l :: ls0) -> F t)
621+
l (@hlist_hd _ _))
622+
| S n0 =>
623+
match nth_error_get_hlist_nth ls0 n0 with
624+
| Some (existT x f) =>
625+
Some (@existT _ (fun t => hlist _ -> F t)
626+
x (fun h : hlist (l :: ls0) => f (hlist_tl h)))
627+
| None => None
629628
end
629+
end
630630
end.
631631

632632
Theorem nth_error_get_hlist_nth_Some

‎theories/Data/Monads/EitherMonad.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Set Implicit Arguments.
55
Set Strict Implicit.
66

77
Import MonadNotation.
8-
Open Local Scope monad_scope.
8+
Local Open Scope monad_scope.
99

1010
Section except.
1111
Variable T : Type.
@@ -95,11 +95,11 @@ Section except.
9595
match x with
9696
| inl s => ret (inl s)
9797
| inr (a,f) => pass (ret (inr a, f))
98-
end)
98+
end)
9999
}.
100100

101101
Global Instance MonadFix_eitherT (MF : MonadFix m) : MonadFix eitherT :=
102-
{ mfix := fun _ _ r v =>
102+
{ mfix := fun _ _ r v =>
103103
mkEitherT (mfix (fun f x => unEitherT (r (fun x => mkEitherT (f x)) x)) v)
104104
}.
105105

‎theories/Data/Monads/OptionMonad.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Set Implicit Arguments.
44
Set Strict Implicit.
55

66
Import MonadNotation.
7-
Open Local Scope monad_scope.
7+
Local Open Scope monad_scope.
88

99
Global Instance Monad_option : Monad option :=
1010
{ ret := @Some

‎theories/Data/PPair.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Section pair.
1515

1616
End pair.
1717

18-
Arguments pprod _ _.
18+
Arguments pprod _ _ : assert.
1919
Arguments ppair {_ _} _ _.
2020
Arguments pfst {_ _} _.
2121
Arguments psnd {_ _} _.

‎theories/Programming/With.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -60,5 +60,5 @@ Delimit Scope struct_scope with record.
6060

6161
Notation "{$ x 'with' y ':=' v $}" := (@wrapWith _ _ x y v _ _) : struct_scope.
6262

63-
Implicit Arguments Next [ T U a b ].
64-
Implicit Arguments Here [ T U a b ].
63+
Arguments Next { T U a b }.
64+
Arguments Here { T U a b }.

‎theories/Structures/MonadCont.v‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
1+
(** The Cont Monad Class
2+
**)
13
Require Import ExtLib.Structures.Monad.
24

3-
Set Implicit Arguments.
4-
Set Maximal Implicit Arguments.
5-
65
Class Cont (m : Type -> Type) : Type :=
7-
{ callCC : forall a b, ((a -> m b) -> m a) -> m a }.
6+
{ callCC : forall a b, ((a -> m b) -> m a) -> m a }.
7+
8+
Arguments callCC {m Cm} {_ _} _ : rename.

‎theories/Structures/MonadExc.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
Require Import ExtLib.Structures.Monad.
22

3-
Set Implicit Arguments.
4-
Set Maximal Implicit Arguments.
5-
6-
Class MonadExc E (m : Type -> Type) : Type :=
3+
Class MonadExc (E : Type) (m : Type -> Type) : Type :=
74
{ raise : forall {T}, E -> m T
85
; catch : forall {T}, m T -> (E -> m T) -> m T
96
}.
7+
8+
Arguments raise {E m mE} {_} _ : rename.
9+
Arguments catch {E m mE} {_} _ _ : rename.

‎theories/Structures/MonadReader.v‎

Lines changed: 26 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,36 @@
1+
(** The Reader Monad Class
2+
**)
13
Require Import ExtLib.Structures.Monad.
24

3-
Set Implicit Arguments.
4-
Set Maximal Implicit Arguments.
5+
Set Universe Polymorphism.
6+
Set Printing Universes.
57

6-
Polymorphic Class MonadReader@{d c} (T : Type@{d}) (m : Type@{d} -> Type@{c})
8+
Class MonadReader@{d c} (T : Type@{d}) (m : Type@{d} -> Type@{c})
79
: Type :=
810
{ local : forall {t : Type@{d}}, (T -> T) -> m t -> m t
911
; ask : m T
1012
}.
1113

12-
Polymorphic Definition asks@{d c}
13-
{m : Type@{d} -> Type@{c}}
14-
{M : Monad m}
15-
{T : Type@{d}}
16-
{MR : MonadReader@{d c} T m}
17-
{U : Type@{d}} (f : T -> U) : m U :=
14+
Arguments local {T} {m} {_} {t} _ _ : rename.
15+
Arguments ask {T} {m} {_} : rename.
16+
17+
Definition asks@{d c}
18+
{m : Type@{d} -> Type@{c}}
19+
{M : Monad m}
20+
{T : Type@{d}}
21+
{MR : MonadReader@{d c} T m}
22+
{U : Type@{d}} (f : T -> U) : m U :=
1823
bind ask (fun x => ret (f x)).
1924

20-
Polymorphic Definition ReaderProd
21-
{m : Type -> Type}
22-
{M : Monad m}
23-
{T S : Type}
24-
{MR : MonadReader T m}
25-
(f : T -> S)
26-
(g : S -> T -> T)
27-
: MonadReader S m :=
28-
{| ask := @asks m M T MR S f
29-
; local := fun _T up (c : m _T) =>
30-
@local T m MR _ (fun s => g (up (f s)) s) c
31-
|}.
25+
Definition ReaderProd@{d c}
26+
{m : Type@{d} -> Type@{c}}
27+
{M : Monad m}
28+
{T S : Type@{d}}
29+
{MR : MonadReader T m}
30+
(f : T -> S)
31+
(g : S -> T -> T)
32+
: MonadReader@{d c} S m :=
33+
{| ask := @asks m M T MR S f
34+
; local := fun _T up (c : m _T) =>
35+
@local T m MR _ (fun s => g (up (f s)) s) c
36+
|}.

0 commit comments

Comments
 (0)