diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-02-13 09:22:58 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-02-13 09:22:58 +0100 |
commit | e9cf693337de2a23f433ce382c14ddc528ebc5f6 (patch) | |
tree | e16e2a167cbc1d4fafe22215fb3d2ee819dc6ed5 /examples | |
parent | 7ad0aff65751133b298ef41861ed8cd688cf18eb (diff) | |
download | smtcoq-e9cf693337de2a23f433ce382c14ddc528ebc5f6.tar.gz smtcoq-e9cf693337de2a23f433ce382c14ddc528ebc5f6.zip |
Updated insertion sort example (fixes #57)
Diffstat (limited to 'examples')
-rw-r--r-- | examples/InsertionSort.v | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/examples/InsertionSort.v b/examples/InsertionSort.v index fcd5dfc..0f21e23 100644 --- a/examples/InsertionSort.v +++ b/examples/InsertionSort.v @@ -21,19 +21,19 @@ definitions - it requires too much from uninterpreted functions even when it is not needed - - it sometimes fails? (may be realted to the previous item) + - it sometimes fails (may be realted to the previous item) *) -Add Rec LoadPath "../src" as SMTCoq. - -Require Import SMTCoq. +Require Import SMTCoq.SMTCoq. Require Import ZArith List Bool. +Local Open Scope Z_scope. + -(* We should really make SMTCoq work with SSReflect! *) +(* This will improve when SMTCoq works with SSReflect! *) -Lemma impl_implb (a b:bool) : (a -> b) <-> (a --> b). +Lemma impl_implb (a b:bool) : (a -> b) <-> (a ---> b). Proof. auto using (reflect_iff _ _ (ReflectFacts.implyP a b)). Qed. @@ -76,20 +76,20 @@ Section InsertionSort. Lemma is_sorted_smaller x y ys : - (((x <=? y) && is_sorted (y :: ys)) --> is_sorted (x :: ys)). + (((x <=? y)%Z && is_sorted (y :: ys)) ---> is_sorted (x :: ys)). Proof. destruct ys as [ |z zs]. - simpl. smt. - change (is_sorted (y :: z :: zs)) with ((y <=? z)%Z && (is_sorted (z::zs))). change (is_sorted (x :: z :: zs)) with ((x <=? z)%Z && (is_sorted (z::zs))). (* [smt] or [verit] fail? *) - assert (H:forall b, (x <=? y) && ((y <=? z) && b) --> (x <=? z) && b) by smt. + assert (H:forall b, (x <=? y)%Z && ((y <=? z) && b) ---> (x <=? z) && b) by smt. apply H. Qed. Lemma is_sorted_cons x xs : - (is_sorted (x::xs)) <--> (is_sorted xs && smaller x xs). + (is_sorted (x::xs)) <---> (is_sorted xs && smaller x xs). Proof. induction xs as [ |y ys IHys]. - reflexivity. @@ -97,27 +97,27 @@ Section InsertionSort. change (smaller x (y :: ys)) with ((x <=? y)%Z && (smaller x ys)). generalize (is_sorted_smaller x y ys). revert IHys. rewrite !impl_implb. (* Idem *) - assert (H:forall a b c d, (a <--> b && c) --> - ((x <=? y) && d --> a) --> - ((x <=? y) && d <--> + assert (H:forall a b c d, (a <---> b && c) ---> + ((x <=? y) && d ---> a) ---> + ((x <=? y) && d <---> d && ((x <=? y) && c))) by smt. apply H. Qed. Lemma insert_keeps_smaller x y ys : - smaller y ys --> (y <=? x) --> smaller y (insert x ys). + smaller y ys ---> (y <=? x) ---> smaller y (insert x ys). Proof. induction ys as [ |z zs IHzs]. - simpl. smt. - simpl. case (x <=? z). + simpl. (* [smt] or [verit] require [Compec (list Z)] but they should not *) - assert (H:forall a, (y <=? z) && a --> (y <=? x) --> (y <=? x) && ((y <=? z) && a)) by smt. + assert (H:forall a, (y <=? z) && a ---> (y <=? x) ---> (y <=? x) && ((y <=? z) && a)) by smt. apply H. + simpl. revert IHzs. rewrite impl_implb. (* Idem *) - assert (H:forall a b, (a --> (y <=? x) --> b) --> (y <=? z) && a --> (y <=? x) --> (y <=? z) && b) by smt. + assert (H:forall a b, (a ---> (y <=? x) ---> b) ---> (y <=? z) && a ---> (y <=? x) ---> (y <=? z) && b) by smt. apply H. Qed. @@ -134,7 +134,7 @@ Section InsertionSort. generalize (insert_keeps_smaller x y ys). revert IHys H Heq. rewrite !impl_implb. (* Idem *) - assert (H: forall a b c d, (a --> b) --> a && c --> negb (x <=? y) --> (c --> (y <=? x) --> d) --> b && d) by smt. + assert (H: forall a b c d, (a ---> b) ---> a && c ---> negb (x <=? y) ---> (c ---> (y <=? x) ---> d) ---> b && d) by smt. apply H. Qed. |