Commit b54d5eda authored by charguer's avatar charguer
Browse files

comparison

parent 43d33b87
......@@ -6,9 +6,25 @@ Require Import Stdlib.
(* Open Scope tag_scope.*)
(*
let compare_int () =
(1 <> 0 && 1 <= 2) || (0 = 1 && 1 >= 2 && 1 < 2 && 2 > 1)
let compare_min () =
(min 0 1)
(********************************************************************)
(********************************************************************)
(* ** List operators *)
let list_ops () =
let x = [1] in
List.length (List.rev (List.concat (List.append [x] [x; x])))
*)
......@@ -18,15 +34,12 @@ Require Import Stdlib.
(********************************************************************)
(*
let compare_options =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
let _r3 = ((Some 3, None) = (None, Some 3)) in
let _r4 = ((Some 3, None) = (Some 3, None)) in
let _r5 = (true = false) in
()
(*
let match_term_when () =
let f x = x + 1 in
match f 3 with
......@@ -553,6 +566,63 @@ Proof using.
Qed.
(********************************************************************)
(* ** Comparison operators *)
Lemma compare_poly_spec :
app compare_poly [tt] \[] \[= tt].
Proof using.
xcf.
xlet_poly_keep (= true). { xapps. typeclass. xsimpl. subst r. logics~. } intro_subst.
xapp. typeclass. intro_subst.
xlet_poly_keep (= true). { xapps. typeclass. xsimpl. subst r. logics~. } intro_subst.
xapp. typeclass. intro_subst.
xrets~.
Qed.
Lemma compare_physical_loc_func_spec :
app compare_physical_loc_func [tt] \[] \[= tt].
Proof using.
xcf. xapps. xapps.
xapp. intro_subst.
xapp. intro_subst.
xfun.
xapp_spec infix_eq_eq_gen_spec. intros.
xlet (\[=1]).
xif.
xapps. xrets~.
xrets~.
intro_subst. xrets~.
Qed.
Fixpoint list_update (k:int) (v:int) (l:list (int*int)) :=
match l with
| nil => nil
| (k2,v2)::t2 =>
let t := (list_update k v t2) in
let v' := (If k = k2 then v else v2) in
(k2,v')::t
end.
Lemma compare_physical_algebraic_spec :
app compare_physical_algebraic [tt] \[] \[= (1,9)::(4,2)::(2,5)::nil ].
Proof using.
xcf. xfun_ind (@list_sub (int*int)) (fun f =>
forall (l:list (int*int)) (k:int) (v:int),
app f [k v l] \[] \[= list_update k v l ]).
{ xmatch.
{ xrets~. }
{ xapps~. xret. xextracts. xif.
{ xrets. case_if. auto. }
{ xapp_spec infix_emark_eq_gen_spec. intros M. xif.
{ xrets. case_if~. }
{ xrets. case_if~. rewrite~ M. } } } }
{ xapps. xsimpl. subst r. simpl. do 3 case_if. auto. }
Qed.
(********************************************************************)
(* ** Inlined total functions *)
......
......@@ -32,43 +32,157 @@ Class PolyComparable (A:Type) (v:A) : Prop :=
Class PolyComparableType (A:Type) : Prop :=
{ polyComparableType : forall (v:A), is_poly_comparable v }.
Axiom is_poly_comparable_int : PolyComparableType loc.
Axiom is_poly_comparable_bool : PolyComparableType int.
Axiom is_poly_comparable_string : PolyComparableType string.
(* todo: char, float *)
Axiom is_poly_comparable_none : forall A, PolyComparable (@None A).
Axiom is_poly_comparable_nil : forall A, PolyComparable (@nil A).
Axiom is_poly_comparable_type_unit :
Lemma PolyComparableType_eq : forall (A:Type),
PolyComparableType A = (forall (v:A), PolyComparable v).
Proof using.
intros. extens. iff H.
{ intros. constructors. applys H. }
{ constructors. intros. applys H. }
Qed.
Lemma PolyComparableType_elim : forall `{PolyComparableType A} (v:A),
PolyComparable v.
Proof using. introv. rewrite PolyComparableType_eq. typeclass. Qed.
(* DO NOT add this lemmas as instance, it makes everything slow. *)
Axiom is_poly_comparable_unit : forall (v:unit),
PolyComparable v.
Axiom is_poly_comparable_int : forall (n:int),
PolyComparable n.
Axiom is_poly_comparable_bool : forall (b:bool),
PolyComparable b.
Axiom is_poly_comparable_char : forall (c:char),
PolyComparable c.
Axiom is_poly_comparable_string : forall (s:string),
PolyComparable s.
Existing Instance is_poly_comparable_unit.
Existing Instance is_poly_comparable_int.
Existing Instance is_poly_comparable_bool.
Existing Instance is_poly_comparable_char.
Existing Instance is_poly_comparable_string.
Axiom is_poly_comparable_none : forall A,
PolyComparable (@None A).
Axiom is_poly_comparable_some : forall A (v:A),
PolyComparable v ->
PolyComparable (Some v).
Axiom is_poly_comparable_nil : forall A,
PolyComparable (@nil A).
Axiom is_poly_comparable_cons : forall A (v:A) (l:list A),
PolyComparable v ->
PolyComparable l ->
PolyComparable (v::l).
Existing Instance is_poly_comparable_none.
Existing Instance is_poly_comparable_some.
Existing Instance is_poly_comparable_nil.
Existing Instance is_poly_comparable_cons.
Global Instance is_poly_comparable_type_unit :
PolyComparableType unit.
Axiom is_poly_comparable_type_int :
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_int :
PolyComparableType int.
Axiom is_poly_comparable_type_bool :
PolyComparableType bool.
Axiom is_poly_comparable_type_option : forall `{PolyComparableType A},
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_bool :
PolyComparableType bool.
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_char :
PolyComparableType char.
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_string :
PolyComparableType string.
Proof using. rewrite PolyComparableType_eq. typeclass. Qed.
Global Instance is_poly_comparable_type_option : forall `{PolyComparableType A},
PolyComparableType (option A).
Axiom is_poly_comparable_type_list : forall `{PolyComparableType A},
Proof using.
introv. do 2 rewrite PolyComparableType_eq. intros.
destruct v; typeclass.
Qed.
Global Instance is_poly_comparable_type_list : forall `{PolyComparableType A},
PolyComparableType (list A).
Proof using.
introv. do 2 rewrite PolyComparableType_eq. intros H l.
induction l; typeclass.
Qed.
Axiom is_poly_comparable_tuple_2 :
forall A1 A2 (v1:A1) (v2:A2),
PolyComparable v1 ->
PolyComparable v2 ->
PolyComparable (v1,v2).
Axiom is_poly_comparable_tuple_3 :
forall A1 A2 A3 (v1:A1) (v2:A2) (v3:A3),
PolyComparable v1 ->
PolyComparable v2 ->
PolyComparable v3 ->
PolyComparable (v1,v2,v3).
Axiom is_poly_comparable_tuple_4 :
forall A1 A2 A3 A4 (v1:A1) (v2:A2) (v3:A3) (v4:A4),
PolyComparable v1 ->
PolyComparable v2 ->
PolyComparable v3 ->
PolyComparable v4 ->
PolyComparable (v1,v2,v3,v4).
Axiom is_poly_comparable_tuple_5 :
forall A1 A2 A3 A4 A5 (v1:A1) (v2:A2) (v3:A3) (v4:A4) (v5:A5),
PolyComparable v1 ->
PolyComparable v2 ->
PolyComparable v3 ->
PolyComparable v4 ->
PolyComparable v5 ->
PolyComparable (v1,v2,v3,v4,v5).
Existing Instance is_poly_comparable_tuple_2.
Existing Instance is_poly_comparable_tuple_3.
Existing Instance is_poly_comparable_tuple_4.
Existing Instance is_poly_comparable_tuple_5.
(* deprecated
Existing Instance is_poly_comparable_type_option.
Existing Instance is_poly_comparable_type_list.
*)
Axiom is_poly_comparable_type_tuple_2 :
Global Instance is_poly_comparable_type_tuple_2 :
forall `{PolyComparableType A1} `{PolyComparableType A2},
PolyComparableType (A1 * A2)%type.
Axiom is_poly_comparable_type_tuple_3 :
Proof using.
intros. rewrite PolyComparableType_eq in *.
intros (v1&v2). typeclass.
Qed.
Global Instance is_poly_comparable_type_tuple_3 :
forall `{PolyComparableType A1} `{PolyComparableType A2} `{PolyComparableType A3},
PolyComparableType (A1 * A2 * A3)%type.
Axiom is_poly_comparable_type_tuple_4 :
Proof using.
intros. rewrite PolyComparableType_eq in *.
intros [[v1 v2] v3]. typeclass.
Qed.
Global Instance is_poly_comparable_type_tuple_4 :
forall `{PolyComparableType A1} `{PolyComparableType A2} `{PolyComparableType A3}
`{PolyComparableType A4},
PolyComparableType (A1 * A2 * A3 * A4)%type.
Axiom is_poly_comparable_type_tuple_5 :
Proof using.
intros. rewrite PolyComparableType_eq in *.
intros [[[v1 v2] v3] v4]. typeclass.
Qed.
Global Instance is_poly_comparable_type_tuple_5 :
forall `{PolyComparableType A1} `{PolyComparableType A2} `{PolyComparableType A3}
`{PolyComparableType A4} `{PolyComparableType A5},
PolyComparableType (A1 * A2 * A3 * A4 * A5)%type.
Axiom is_poly_comparable_type_tuple_6 :
forall `{PolyComparableType A1} `{PolyComparableType A2} `{PolyComparableType A3}
`{PolyComparableType A4} `{PolyComparableType A5} `{PolyComparableType A6},
PolyComparableType (A1 * A2 * A3 * A4 * A5 * A6)%type.
Proof using.
intros. rewrite PolyComparableType_eq in *.
intros [[[[v1 v2] v3] v4] v5]. typeclass.
Qed.
(********************************************************************)
......
......@@ -3070,7 +3070,11 @@ Tactic Notation "xrecord_new" :=
*)
(** Debugging for [xapp]:
- [xapp_types] show the types involved in the [app] instances.
- [xapp_types] show the types involved in the [app] instances
in the goal and in the specification found.
- [xapp_spec_types P] show the types involved in the [app] instances
in the goal and in the specification [P] provided.
- [xapp1] sets the goal in the right form for [xapp],
by calling [xseq] or [xlet], or [xgc_post] if applicable
......@@ -3459,20 +3463,36 @@ Tactic Notation "xapps_skip" :=
(** [xapp_types] *)
Ltac xapp_types_core_noarg tt :=
xapp_prepare_goal ltac:(fun _ => idtac);
idtac "=== type of app in goal ===";
cfml_show_app_type_goal tt;
idtac "=== type of app in spec === ";
let S := fresh "Spec" in
xapp_use_or_find ___ S;
forwards_nounfold_skip_sides_then S ltac:(fun K =>
let T := type of K in
cfml_show_app_type T);
clear S.
xapp_prepare_goal ltac:(fun _ =>
idtac "=== type of app in goal ===";
cfml_show_app_type_goal tt;
idtac "=== type of app in spec === ";
let S := fresh "Spec" in
xapp_use_or_find ___ S;
forwards_nounfold_skip_sides_then S ltac:(fun K =>
let T := type of K in
cfml_show_app_type T);
clear S).
(* TODO: fix bug: need to take proj2 if spec lemma *)
Tactic Notation "xapp_types" :=
xapp_types_core_noarg tt.
(** [xapp_spec_types] *)
(* TODO :factorize better;
TODO: same bug as above *)
Ltac xapp_spec_types_core_noarg S :=
xapp_prepare_goal ltac:(fun _ =>
idtac "=== type of app in goal ===";
cfml_show_app_type_goal tt;
idtac "=== type of app in spec === ";
forwards_nounfold_skip_sides_then S ltac:(fun K =>
let T := type of K in
cfml_show_app_type T)).
Tactic Notation "xapp_spec_types" constr(S) :=
xapp_spec_types_core_noarg S.
(* DEPRECATED
......@@ -3746,7 +3766,7 @@ Ltac xcf_core_app f :=
xcf_core_app_exploit H. (* todo: might need sapply here *)
Ltac xcf_fallback f :=
idtac "Warning: could not exploit the specification; maybe the types don't match; check them using [xcf_debug]; if you intend to use the specification manually, use [xcf_show as S].";
idtac "Warning: could not exploit the specification; maybe the types don't match; check them using [xcf_types]; if you intend to use the specification manually, use [xcf_show as S].";
xcf_find f;
let Sf := fresh "Spec" in
intros Sf.
......
Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml.
Generalizable Variable A.
(************************************************************)
......@@ -59,26 +59,33 @@ Hint Extern 1 (RegisterSpec infix_emark_eq__) => Provide infix_emark_eq_loc_spec
(************************************************************)
(** Comparison *)
Definition eq_spec_for (A:Type) := curried 2%nat infix_eq__ /\
forall (a b:bool),
Parameter infix_eq_spec : curried 2%nat infix_eq__ /\
forall A (a b : A),
(PolyComparable a \/ PolyComparable b) ->
app infix_eq__ [a b] \[] \[= isTrue (a = b) ].
Parameter eq_bool_spec : eq_spec_for bool.
Parameter eq_int_spec : eq_spec_for int.
Hint Extern 1 (RegisterSpec infix_eq__) => Provide infix_eq_spec.
Hint Extern 1 (RegisterSpec infix_eq__) => Provide eq_int_spec.
(* TODO: register several specs *)
Lemma infix_eq_spec_simple :
forall `{PolyComparableType A} (a b : A),
app infix_eq__ [a b] \[] \[= isTrue (a = b) ].
Proof using.
intros. xapp. left. constructor. applys polyComparableType.
Qed.
Definition neq_spec_for (A:Type) := curried 2%nat infix_lt_gt__ /\
forall (a b:bool),
Parameter infix_neq_spec : curried 2%nat infix_eq__ /\
forall A (a b : A),
(PolyComparable a \/ PolyComparable b) ->
app infix_lt_gt__ [a b] \[] \[= isTrue (a <> b) ].
Parameter neq_bool_spec : neq_spec_for bool.
Parameter neq_int_spec : neq_spec_for int.
Hint Extern 1 (RegisterSpec infix_lt_gt__) => Provide neq_int_spec.
Lemma infix_neq_spec_simple :
forall `{PolyComparableType A} (a b : A),
app infix_lt_gt__ [a b] \[] \[= isTrue (a <> b) ].
Proof using.
intros. xapp. left. constructor. applys polyComparableType.
Qed.
(* LATER: give specification for partially applied comparison operators *)
Hint Extern 1 (RegisterSpec infix_lt_gt__) => Provide infix_neq_spec.
Lemma min_spec : forall (n m:int),
app min [n m] \[] \[= Coq.ZArith.BinInt.Zmin n m ].
......
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