Commit a64b8e39 authored by Robbert Krebbers's avatar Robbert Krebbers

Set Obligation Tactic := idtac globally.

parent 504f25ae
......@@ -8,6 +8,7 @@ Global Generalizable All Variables.
Global Set Automatic Coercions Import.
Global Set Asymmetric Patterns.
Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
Obligation Tactic := idtac.
(** * General *)
(** Zipping lists. *)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export prelude.list.
Local Obligation Tactic := idtac.
Local Open Scope positive.
Class Countable A `{ x y : A, Decision (x = y)} := {
......
......@@ -93,15 +93,15 @@ Proof.
Defined.
Global Program Instance collection_subseteq_dec_slow (X Y : C) :
Decision (X Y) | 100 :=
match decide_rel (=) (size (X Y)) 0 with
| left E1 => left _ | right E1 => right _
match decide_rel (=) (size (X Y)) 0 return _ with
| left _ => left _ | right _ => right _
end.
Next Obligation.
intros x Ex; apply dec_stable; intro. destruct (proj1 (elem_of_empty x)).
intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)).
apply (size_empty_inv _ E1). by rewrite elem_of_difference.
Qed.
Next Obligation.
intros E2. destruct E1. apply size_empty_iff, equiv_empty. intros x.
intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x.
rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
Qed.
Lemma size_union_alt X Y : size (X Y) = size X + size (Y X).
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export prelude.countable prelude.list.
Obligation Tactic := idtac.
Class Finite A `{ x y : A, Decision (x = y)} := {
enum : list A;
......
......@@ -25,14 +25,14 @@ Next Obligation. by intros n X; simpl_map. Qed.
Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
Hashset {[ hash x [x] ]} _.
Next Obligation.
intros n l. rewrite lookup_singleton_Some. intros [<- <-].
intros x n l [<- <-]%lookup_singleton_Some.
rewrite Forall_singleton; auto using NoDup_singleton.
Qed.
Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _.
Next Obligation.
intros n l'. rewrite lookup_union_with_Some.
intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_equality'; auto.
split; [apply Forall_list_union|apply NoDup_list_union];
first [by eapply Hm1; eauto | by eapply Hm2; eauto].
......@@ -42,7 +42,7 @@ Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
Hashset (intersection_with (λ l k,
let l' := list_intersection l k in guard (l' []); Some l') m1 m2) _.
Next Obligation.
intros n l'. rewrite lookup_intersection_with_Some.
intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_intersection_with_Some.
intros (?&?&?&?&?); simplify_option_equality.
split; [apply Forall_list_intersection|apply NoDup_list_intersection];
first [by eapply Hm1; eauto | by eapply Hm2; eauto].
......@@ -52,7 +52,7 @@ Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
Hashset (difference_with (λ l k,
let l' := list_difference l k in guard (l' []); Some l') m1 m2) _.
Next Obligation.
intros n l'. rewrite lookup_difference_with_Some.
intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_difference_with_Some.
intros [[??]|(?&?&?&?&?)]; simplify_option_equality; auto.
split; [apply Forall_list_difference|apply NoDup_list_difference];
first [by eapply Hm1; eauto | by eapply Hm2; eauto].
......
......@@ -189,17 +189,11 @@ Proof. by injection 1. Qed.
Instance N_eq_dec: x y : N, Decision (x = y) := N.eq_dec.
Program Instance N_le_dec (x y : N) : Decision (x y)%N :=
match Ncompare x y with
| Gt => right _
| _ => left _
end.
Next Obligation. congruence. Qed.
match Ncompare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
match Ncompare x y with
| Lt => left _
| _ => right _
end.
Next Obligation. congruence. Qed.
match Ncompare x y with Lt => left _ | _ => right _ end.
Solve Obligations with naive_solver.
Instance N_inhabited: Inhabited N := populate 1%N.
Instance: PartialOrder ()%N.
Proof.
......@@ -340,10 +334,12 @@ Arguments Qred _ : simpl never.
Instance Qc_eq_dec: x y : Qc, Decision (x = y) := Qc_eq_dec.
Program Instance Qc_le_dec (x y : Qc) : Decision (x y) :=
if Qclt_le_dec y x then right _ else left _.
Next Obligation. by apply Qclt_not_le. Qed.
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y) :=
if Qclt_le_dec x y then left _ else right _.
Next Obligation. by apply Qcle_not_lt. Qed.
Solve Obligations with done.
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
Instance: PartialOrder ().
Proof.
......
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