Commit 8d0efe8e authored by Ralf Jung's avatar Ralf Jung

remove Set Asymmetric Patterns

parent c53cefcd
......@@ -5,7 +5,6 @@ that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, collections, and various other data
structures. *)
Global Generalizable All Variables.
Global Set Asymmetric Patterns.
Global Unset Transparent Obligations.
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
Set Default Proof Using "Type".
......
......@@ -28,7 +28,7 @@ Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope.
Notation "10" := (FS 9) : fin_scope.
Fixpoint fin_to_nat {n} (i : fin n) : nat :=
match i with 0%fin => 0 | FS _ i => S (fin_to_nat i) end.
match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.
Coercion fin_to_nat : fin >-> nat.
Notation fin_of_nat := Fin.of_nat_lt.
......@@ -57,7 +57,7 @@ Definition fin_S_inv {n} (P : fin (S n) → Type)
(H0 : P 0%fin) (HS : i, P (FS i)) (i : fin (S n)) : P i.
Proof.
revert P H0 HS.
refine match i with 0%fin => λ _ H0 _, H0 | FS _ i => λ _ _ HS, HS i end.
refine match i with 0%fin => λ _ H0 _, H0 | FS i => λ _ _ HS, HS i end.
Defined.
Ltac inv_fin i :=
......
......@@ -72,7 +72,7 @@ Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
Fin.of_nat_lt (encode_lt_card x).
Program Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
match Some_dec (decode_nat i) return _ with
| inleft (exist x _) => x | inright _ => _
| inleft (exist _ x _) => x | inright _ => _
end.
Next Obligation.
intros A ?? i ?; exfalso.
......
......@@ -14,12 +14,12 @@ Inductive hlist : tlist → Type :=
Fixpoint tapp (As Bs : tlist) : tlist :=
match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
match xs with hnil => ys | hcons _ _ x xs => hcons x (happ xs ys) end.
match xs with hnil => ys | hcons x xs => hcons x (happ xs ys) end.
Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
match xs with hnil => () | hcons _ _ x _ => x end.
match xs with hnil => () | hcons x _ => x end.
Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
match xs with hnil => () | hcons _ _ _ xs => xs end.
match xs with hnil => () | hcons _ xs => xs end.
Fixpoint hheads {As Bs} : hlist (tapp As Bs) hlist As :=
match As with
......@@ -43,7 +43,7 @@ Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
(fix go As xs :=
match xs in hlist As return himpl As B B with
| hnil => λ f, f
| hcons A As x xs => λ f, go As xs (f x)
| @hcons A As x xs => λ f, go As xs (f x)
end) _ xs f.
Coercion hcurry : himpl >-> Funclass.
......
......@@ -65,7 +65,7 @@ Proof.
set (f mx := match mx return P mx is_Some mx with
Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
set (g mx (H : is_Some mx) :=
match H return P mx with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end).
match H return P mx with ex_intro _ _ p => eq_rect _ _ I _ (eq_sym p) end).
assert ( mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst).
intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
Qed.
......
......@@ -238,7 +238,7 @@ Qed.
Fixpoint vinsert {A n} (i : fin n) (x : A) : vec A n vec A n :=
match i with
| 0%fin => vec_S_inv _ (λ _ v, x ::: v)
| FS _ i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
| FS i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
end.
Lemma vec_to_list_insert {A n} i x (v : vec A n) :
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment