From b4c72e883127237fe32a7f4ee21610f1c87148bb Mon Sep 17 00:00:00 2001
From: Ike Mulder <i.mulder@cs.ru.nl>
Date: Tue, 24 Nov 2020 15:37:49 +0100
Subject: [PATCH] =?UTF-8?q?Add=20simplification=20instance=20for=20list=20?=
 =?UTF-8?q?=E2=89=A0=20[],=20needed=20for=20quicksort?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/lithium/simpl_instances.v            |   4 +
 .../quicksort_exercise/generated_code.v       | 107 ++++++-
 .../generated_proof_quicksort.v               |   1 +
 .../quicksort_exercise/generated_spec.v       |   2 +
 .../proofs/quicksort_exercise/proof_files     |   1 +
 .../quicksort_solution/generated_code.v       | 267 ++++++++++++------
 .../generated_proof_append.v                  |   1 +
 .../generated_proof_partition.v               |   1 +
 .../generated_proof_quicksort.v               |  31 ++
 .../quicksort_solution/generated_spec.v       |   8 +-
 .../proofs/quicksort_solution/list_proofs.v   |  66 +++++
 .../proofs/quicksort_solution/proof_files     |   1 +
 tutorial/quicksort_exercise.c                 |  14 +-
 tutorial/quicksort_solution.c                 |  26 +-
 14 files changed, 426 insertions(+), 104 deletions(-)
 create mode 100644 tutorial/proofs/quicksort_exercise/generated_proof_quicksort.v
 create mode 100644 tutorial/proofs/quicksort_solution/generated_proof_quicksort.v
 create mode 100644 tutorial/proofs/quicksort_solution/list_proofs.v

diff --git a/theories/lithium/simpl_instances.v b/theories/lithium/simpl_instances.v
index 82d38d50..5786737a 100644
--- a/theories/lithium/simpl_instances.v
+++ b/theories/lithium/simpl_instances.v
@@ -39,6 +39,10 @@ Proof. split; destruct l; naive_solver. Qed.
 Global Instance simpl_to_cons_Some A (l : list A) x : SimplBothRel (=) (maybe2 cons l) (Some x) (l = x.1::x.2).
 Proof. split; destruct l, x; naive_solver. Qed.
 
+Global Instance simpl_protected_neq_nil A (l : list A) `{!IsProtected l} :
+  SimplBoth (l ≠ []) (∃ x l', l = x :: l').
+Proof. split; destruct l; naive_solver. Qed.
+
 Global Instance simpl_gt_0_neg n : SimplBoth (¬ (0 < n))%nat (n = 0%nat).
 Proof. split; destruct n; naive_solver lia. Qed.
 
diff --git a/tutorial/proofs/quicksort_exercise/generated_code.v b/tutorial/proofs/quicksort_exercise/generated_code.v
index e43d90b0..f096b27c 100644
--- a/tutorial/proofs/quicksort_exercise/generated_code.v
+++ b/tutorial/proofs/quicksort_exercise/generated_code.v
@@ -65,14 +65,14 @@ Section code.
   Definition loc_60 : location_info := LocationInfo file_0 40 13 40 17.
   Definition loc_61 : location_info := LocationInfo file_0 40 13 40 17.
   Definition loc_62 : location_info := LocationInfo file_0 35 7 35 25.
-  Definition loc_63 : location_info := LocationInfo file_0 35 7 35 16.
-  Definition loc_64 : location_info := LocationInfo file_0 35 7 35 16.
-  Definition loc_65 : location_info := LocationInfo file_0 35 7 35 11.
-  Definition loc_66 : location_info := LocationInfo file_0 35 7 35 11.
-  Definition loc_67 : location_info := LocationInfo file_0 35 9 35 10.
-  Definition loc_68 : location_info := LocationInfo file_0 35 9 35 10.
-  Definition loc_69 : location_info := LocationInfo file_0 35 20 35 25.
-  Definition loc_70 : location_info := LocationInfo file_0 35 20 35 25.
+  Definition loc_63 : location_info := LocationInfo file_0 35 7 35 12.
+  Definition loc_64 : location_info := LocationInfo file_0 35 7 35 12.
+  Definition loc_65 : location_info := LocationInfo file_0 35 16 35 25.
+  Definition loc_66 : location_info := LocationInfo file_0 35 16 35 25.
+  Definition loc_67 : location_info := LocationInfo file_0 35 16 35 20.
+  Definition loc_68 : location_info := LocationInfo file_0 35 16 35 20.
+  Definition loc_69 : location_info := LocationInfo file_0 35 18 35 19.
+  Definition loc_70 : location_info := LocationInfo file_0 35 18 35 19.
   Definition loc_71 : location_info := LocationInfo file_0 34 18 34 20.
   Definition loc_72 : location_info := LocationInfo file_0 34 18 34 20.
   Definition loc_73 : location_info := LocationInfo file_0 34 19 34 20.
@@ -94,6 +94,48 @@ Section code.
   Definition loc_93 : location_info := LocationInfo file_0 30 6 30 7.
   Definition loc_94 : location_info := LocationInfo file_0 30 6 30 7.
   Definition loc_95 : location_info := LocationInfo file_0 30 11 30 25.
+  Definition loc_98 : location_info := LocationInfo file_0 46 2 54 3.
+  Definition loc_99 : location_info := LocationInfo file_0 46 27 48 3.
+  Definition loc_100 : location_info := LocationInfo file_0 47 4 47 11.
+  Definition loc_102 : location_info := LocationInfo file_0 48 9 54 3.
+  Definition loc_103 : location_info := LocationInfo file_0 49 4 49 26.
+  Definition loc_104 : location_info := LocationInfo file_0 50 4 50 40.
+  Definition loc_105 : location_info := LocationInfo file_0 51 4 51 23.
+  Definition loc_106 : location_info := LocationInfo file_0 52 4 52 17.
+  Definition loc_107 : location_info := LocationInfo file_0 53 4 53 22.
+  Definition loc_108 : location_info := LocationInfo file_0 53 4 53 10.
+  Definition loc_109 : location_info := LocationInfo file_0 53 4 53 10.
+  Definition loc_110 : location_info := LocationInfo file_0 53 11 53 12.
+  Definition loc_111 : location_info := LocationInfo file_0 53 11 53 12.
+  Definition loc_112 : location_info := LocationInfo file_0 53 14 53 20.
+  Definition loc_113 : location_info := LocationInfo file_0 53 14 53 20.
+  Definition loc_114 : location_info := LocationInfo file_0 52 4 52 13.
+  Definition loc_115 : location_info := LocationInfo file_0 52 4 52 13.
+  Definition loc_116 : location_info := LocationInfo file_0 52 14 52 15.
+  Definition loc_117 : location_info := LocationInfo file_0 52 14 52 15.
+  Definition loc_118 : location_info := LocationInfo file_0 51 4 51 13.
+  Definition loc_119 : location_info := LocationInfo file_0 51 4 51 13.
+  Definition loc_120 : location_info := LocationInfo file_0 51 14 51 21.
+  Definition loc_121 : location_info := LocationInfo file_0 51 15 51 21.
+  Definition loc_122 : location_info := LocationInfo file_0 50 20 50 39.
+  Definition loc_123 : location_info := LocationInfo file_0 50 20 50 29.
+  Definition loc_124 : location_info := LocationInfo file_0 50 20 50 29.
+  Definition loc_125 : location_info := LocationInfo file_0 50 30 50 31.
+  Definition loc_126 : location_info := LocationInfo file_0 50 30 50 31.
+  Definition loc_127 : location_info := LocationInfo file_0 50 33 50 38.
+  Definition loc_128 : location_info := LocationInfo file_0 50 33 50 38.
+  Definition loc_131 : location_info := LocationInfo file_0 49 16 49 25.
+  Definition loc_132 : location_info := LocationInfo file_0 49 16 49 25.
+  Definition loc_133 : location_info := LocationInfo file_0 49 16 49 20.
+  Definition loc_134 : location_info := LocationInfo file_0 49 16 49 20.
+  Definition loc_135 : location_info := LocationInfo file_0 49 18 49 19.
+  Definition loc_136 : location_info := LocationInfo file_0 49 18 49 19.
+  Definition loc_139 : location_info := LocationInfo file_0 46 5 46 25.
+  Definition loc_140 : location_info := LocationInfo file_0 46 5 46 7.
+  Definition loc_141 : location_info := LocationInfo file_0 46 5 46 7.
+  Definition loc_142 : location_info := LocationInfo file_0 46 6 46 7.
+  Definition loc_143 : location_info := LocationInfo file_0 46 6 46 7.
+  Definition loc_144 : location_info := LocationInfo file_0 46 11 46 25.
 
   (* Definition of struct [list_node]. *)
   Program Definition struct_list_node := {|
@@ -176,7 +218,7 @@ Section code.
         "head" <-{ LPtr }
           LocInfoE loc_71 (use{LPtr} (LocInfoE loc_73 (!{LPtr} (LocInfoE loc_74 ("l"))))) ;
         locinfo: loc_62 ;
-        if: LocInfoE loc_62 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_62 ((LocInfoE loc_63 (use{it_layout i32} (LocInfoE loc_64 ((LocInfoE loc_65 (!{LPtr} (LocInfoE loc_67 (!{LPtr} (LocInfoE loc_68 ("l")))))) at{struct_list_node} "val")))) ≤{IntOp i32, IntOp i32} (LocInfoE loc_69 (use{it_layout i32} (LocInfoE loc_70 ("pivot")))))))
+        if: LocInfoE loc_62 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_62 ((LocInfoE loc_63 (use{it_layout i32} (LocInfoE loc_64 ("pivot")))) ≤{IntOp i32, IntOp i32} (LocInfoE loc_65 (use{it_layout i32} (LocInfoE loc_66 ((LocInfoE loc_67 (!{LPtr} (LocInfoE loc_69 (!{LPtr} (LocInfoE loc_70 ("l")))))) at{struct_list_node} "val")))))))
         then
         locinfo: loc_39 ;
           Goto "#3"
@@ -200,4 +242,51 @@ Section code.
       ]> $∅
     )%E
   |}.
+
+  (* Definition of function [quicksort]. *)
+  Definition impl_quicksort (append partition quicksort : loc): function := {|
+    f_args := [
+      ("l", LPtr)
+    ];
+    f_local_vars := [
+      ("pivot", it_layout i32);
+      ("higher", LPtr)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_139 ;
+        if: LocInfoE loc_139 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_139 ((LocInfoE loc_140 (use{LPtr} (LocInfoE loc_142 (!{LPtr} (LocInfoE loc_143 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_144 (NULL)))))
+        then
+        locinfo: loc_100 ;
+          Goto "#1"
+        else
+        Goto "#2"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_100 ;
+        Return (VOID)
+      ]> $
+      <[ "#2" :=
+        "pivot" <-{ it_layout i32 }
+          LocInfoE loc_131 (use{it_layout i32} (LocInfoE loc_132 ((LocInfoE loc_133 (!{LPtr} (LocInfoE loc_135 (!{LPtr} (LocInfoE loc_136 ("l")))))) at{struct_list_node} "val"))) ;
+        locinfo: loc_122 ;
+        "$0" <- LocInfoE loc_124 (partition) with
+          [ LocInfoE loc_125 (use{LPtr} (LocInfoE loc_126 ("l"))) ;
+          LocInfoE loc_127 (use{it_layout i32} (LocInfoE loc_128 ("pivot"))) ] ;
+        "higher" <-{ LPtr } LocInfoE loc_122 ("$0") ;
+        locinfo: loc_105 ;
+        "_" <- LocInfoE loc_119 (quicksort) with
+          [ LocInfoE loc_120 (&(LocInfoE loc_121 ("higher"))) ] ;
+        locinfo: loc_106 ;
+        "_" <- LocInfoE loc_115 (quicksort) with
+          [ LocInfoE loc_116 (use{LPtr} (LocInfoE loc_117 ("l"))) ] ;
+        locinfo: loc_107 ;
+        "_" <- LocInfoE loc_109 (append) with
+          [ LocInfoE loc_110 (use{LPtr} (LocInfoE loc_111 ("l"))) ;
+          LocInfoE loc_112 (use{LPtr} (LocInfoE loc_113 ("higher"))) ] ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
 End code.
diff --git a/tutorial/proofs/quicksort_exercise/generated_proof_quicksort.v b/tutorial/proofs/quicksort_exercise/generated_proof_quicksort.v
new file mode 100644
index 00000000..7afb1f35
--- /dev/null
+++ b/tutorial/proofs/quicksort_exercise/generated_proof_quicksort.v
@@ -0,0 +1 @@
+(* You were too lazy to even write a spec for this function. *)
diff --git a/tutorial/proofs/quicksort_exercise/generated_spec.v b/tutorial/proofs/quicksort_exercise/generated_spec.v
index 1dc22b0b..68467134 100644
--- a/tutorial/proofs/quicksort_exercise/generated_spec.v
+++ b/tutorial/proofs/quicksort_exercise/generated_spec.v
@@ -11,4 +11,6 @@ Section spec.
   (* Function [append] has been skipped. *)
 
   (* Function [partition] has been skipped. *)
+
+  (* Function [quicksort] has been skipped. *)
 End spec.
diff --git a/tutorial/proofs/quicksort_exercise/proof_files b/tutorial/proofs/quicksort_exercise/proof_files
index 0b5500e1..97f3be09 100644
--- a/tutorial/proofs/quicksort_exercise/proof_files
+++ b/tutorial/proofs/quicksort_exercise/proof_files
@@ -1,2 +1,3 @@
 generated_proof_append.v
 generated_proof_partition.v
+generated_proof_quicksort.v
diff --git a/tutorial/proofs/quicksort_solution/generated_code.v b/tutorial/proofs/quicksort_solution/generated_code.v
index d1f7479c..44fd2849 100644
--- a/tutorial/proofs/quicksort_solution/generated_code.v
+++ b/tutorial/proofs/quicksort_solution/generated_code.v
@@ -6,94 +6,136 @@ Set Default Proof Using "Type".
 (* Generated from [tutorial/quicksort_solution.c]. *)
 Section code.
   Definition file_0 : string := "tutorial/quicksort_solution.c".
-  Definition loc_2 : location_info := LocationInfo file_0 24 2 28 3.
-  Definition loc_3 : location_info := LocationInfo file_0 24 27 26 3.
-  Definition loc_4 : location_info := LocationInfo file_0 25 4 25 11.
-  Definition loc_5 : location_info := LocationInfo file_0 25 4 25 6.
-  Definition loc_6 : location_info := LocationInfo file_0 25 5 25 6.
-  Definition loc_7 : location_info := LocationInfo file_0 25 5 25 6.
-  Definition loc_8 : location_info := LocationInfo file_0 25 9 25 10.
-  Definition loc_9 : location_info := LocationInfo file_0 25 9 25 10.
-  Definition loc_10 : location_info := LocationInfo file_0 26 9 28 3.
-  Definition loc_11 : location_info := LocationInfo file_0 27 4 27 27.
-  Definition loc_12 : location_info := LocationInfo file_0 27 4 27 10.
-  Definition loc_13 : location_info := LocationInfo file_0 27 4 27 10.
-  Definition loc_14 : location_info := LocationInfo file_0 27 11 27 22.
-  Definition loc_15 : location_info := LocationInfo file_0 27 12 27 22.
-  Definition loc_16 : location_info := LocationInfo file_0 27 12 27 16.
-  Definition loc_17 : location_info := LocationInfo file_0 27 12 27 16.
-  Definition loc_18 : location_info := LocationInfo file_0 27 14 27 15.
-  Definition loc_19 : location_info := LocationInfo file_0 27 14 27 15.
-  Definition loc_20 : location_info := LocationInfo file_0 27 24 27 25.
-  Definition loc_21 : location_info := LocationInfo file_0 27 24 27 25.
-  Definition loc_22 : location_info := LocationInfo file_0 24 5 24 25.
-  Definition loc_23 : location_info := LocationInfo file_0 24 5 24 7.
-  Definition loc_24 : location_info := LocationInfo file_0 24 5 24 7.
-  Definition loc_25 : location_info := LocationInfo file_0 24 6 24 7.
-  Definition loc_26 : location_info := LocationInfo file_0 24 6 24 7.
-  Definition loc_27 : location_info := LocationInfo file_0 24 11 24 25.
-  Definition loc_30 : location_info := LocationInfo file_0 39 2 51 3.
-  Definition loc_31 : location_info := LocationInfo file_0 39 27 41 3.
-  Definition loc_32 : location_info := LocationInfo file_0 40 4 40 26.
-  Definition loc_33 : location_info := LocationInfo file_0 40 11 40 25.
-  Definition loc_34 : location_info := LocationInfo file_0 41 9 51 3.
-  Definition loc_35 : location_info := LocationInfo file_0 42 4 42 48.
-  Definition loc_36 : location_info := LocationInfo file_0 43 4 43 21.
-  Definition loc_37 : location_info := LocationInfo file_0 44 4 50 5.
-  Definition loc_38 : location_info := LocationInfo file_0 44 27 48 5.
-  Definition loc_39 : location_info := LocationInfo file_0 45 6 45 22.
-  Definition loc_40 : location_info := LocationInfo file_0 46 6 46 24.
-  Definition loc_41 : location_info := LocationInfo file_0 47 6 47 18.
-  Definition loc_42 : location_info := LocationInfo file_0 47 13 47 17.
-  Definition loc_43 : location_info := LocationInfo file_0 47 13 47 17.
-  Definition loc_44 : location_info := LocationInfo file_0 46 6 46 16.
-  Definition loc_45 : location_info := LocationInfo file_0 46 6 46 10.
-  Definition loc_46 : location_info := LocationInfo file_0 46 6 46 10.
-  Definition loc_47 : location_info := LocationInfo file_0 46 19 46 23.
-  Definition loc_48 : location_info := LocationInfo file_0 46 19 46 23.
-  Definition loc_49 : location_info := LocationInfo file_0 45 6 45 8.
-  Definition loc_50 : location_info := LocationInfo file_0 45 7 45 8.
-  Definition loc_51 : location_info := LocationInfo file_0 45 7 45 8.
-  Definition loc_52 : location_info := LocationInfo file_0 45 11 45 21.
-  Definition loc_53 : location_info := LocationInfo file_0 45 11 45 21.
-  Definition loc_54 : location_info := LocationInfo file_0 45 11 45 15.
-  Definition loc_55 : location_info := LocationInfo file_0 45 11 45 15.
-  Definition loc_56 : location_info := LocationInfo file_0 45 13 45 14.
-  Definition loc_57 : location_info := LocationInfo file_0 45 13 45 14.
-  Definition loc_58 : location_info := LocationInfo file_0 48 11 50 5.
-  Definition loc_59 : location_info := LocationInfo file_0 49 6 49 18.
-  Definition loc_60 : location_info := LocationInfo file_0 49 13 49 17.
-  Definition loc_61 : location_info := LocationInfo file_0 49 13 49 17.
-  Definition loc_62 : location_info := LocationInfo file_0 44 7 44 25.
-  Definition loc_63 : location_info := LocationInfo file_0 44 7 44 16.
-  Definition loc_64 : location_info := LocationInfo file_0 44 7 44 16.
-  Definition loc_65 : location_info := LocationInfo file_0 44 7 44 11.
-  Definition loc_66 : location_info := LocationInfo file_0 44 7 44 11.
-  Definition loc_67 : location_info := LocationInfo file_0 44 9 44 10.
-  Definition loc_68 : location_info := LocationInfo file_0 44 9 44 10.
-  Definition loc_69 : location_info := LocationInfo file_0 44 20 44 25.
-  Definition loc_70 : location_info := LocationInfo file_0 44 20 44 25.
-  Definition loc_71 : location_info := LocationInfo file_0 43 18 43 20.
-  Definition loc_72 : location_info := LocationInfo file_0 43 18 43 20.
-  Definition loc_73 : location_info := LocationInfo file_0 43 19 43 20.
-  Definition loc_74 : location_info := LocationInfo file_0 43 19 43 20.
-  Definition loc_77 : location_info := LocationInfo file_0 42 18 42 47.
-  Definition loc_78 : location_info := LocationInfo file_0 42 18 42 27.
-  Definition loc_79 : location_info := LocationInfo file_0 42 18 42 27.
-  Definition loc_80 : location_info := LocationInfo file_0 42 28 42 39.
-  Definition loc_81 : location_info := LocationInfo file_0 42 29 42 39.
-  Definition loc_82 : location_info := LocationInfo file_0 42 29 42 33.
-  Definition loc_83 : location_info := LocationInfo file_0 42 29 42 33.
-  Definition loc_84 : location_info := LocationInfo file_0 42 31 42 32.
-  Definition loc_85 : location_info := LocationInfo file_0 42 31 42 32.
-  Definition loc_86 : location_info := LocationInfo file_0 42 41 42 46.
-  Definition loc_87 : location_info := LocationInfo file_0 42 41 42 46.
-  Definition loc_90 : location_info := LocationInfo file_0 39 5 39 25.
-  Definition loc_91 : location_info := LocationInfo file_0 39 5 39 7.
-  Definition loc_92 : location_info := LocationInfo file_0 39 5 39 7.
-  Definition loc_93 : location_info := LocationInfo file_0 39 6 39 7.
-  Definition loc_94 : location_info := LocationInfo file_0 39 6 39 7.
-  Definition loc_95 : location_info := LocationInfo file_0 39 11 39 25.
+  Definition loc_2 : location_info := LocationInfo file_0 26 2 30 3.
+  Definition loc_3 : location_info := LocationInfo file_0 26 27 28 3.
+  Definition loc_4 : location_info := LocationInfo file_0 27 4 27 11.
+  Definition loc_5 : location_info := LocationInfo file_0 27 4 27 6.
+  Definition loc_6 : location_info := LocationInfo file_0 27 5 27 6.
+  Definition loc_7 : location_info := LocationInfo file_0 27 5 27 6.
+  Definition loc_8 : location_info := LocationInfo file_0 27 9 27 10.
+  Definition loc_9 : location_info := LocationInfo file_0 27 9 27 10.
+  Definition loc_10 : location_info := LocationInfo file_0 28 9 30 3.
+  Definition loc_11 : location_info := LocationInfo file_0 29 4 29 27.
+  Definition loc_12 : location_info := LocationInfo file_0 29 4 29 10.
+  Definition loc_13 : location_info := LocationInfo file_0 29 4 29 10.
+  Definition loc_14 : location_info := LocationInfo file_0 29 11 29 22.
+  Definition loc_15 : location_info := LocationInfo file_0 29 12 29 22.
+  Definition loc_16 : location_info := LocationInfo file_0 29 12 29 16.
+  Definition loc_17 : location_info := LocationInfo file_0 29 12 29 16.
+  Definition loc_18 : location_info := LocationInfo file_0 29 14 29 15.
+  Definition loc_19 : location_info := LocationInfo file_0 29 14 29 15.
+  Definition loc_20 : location_info := LocationInfo file_0 29 24 29 25.
+  Definition loc_21 : location_info := LocationInfo file_0 29 24 29 25.
+  Definition loc_22 : location_info := LocationInfo file_0 26 5 26 25.
+  Definition loc_23 : location_info := LocationInfo file_0 26 5 26 7.
+  Definition loc_24 : location_info := LocationInfo file_0 26 5 26 7.
+  Definition loc_25 : location_info := LocationInfo file_0 26 6 26 7.
+  Definition loc_26 : location_info := LocationInfo file_0 26 6 26 7.
+  Definition loc_27 : location_info := LocationInfo file_0 26 11 26 25.
+  Definition loc_30 : location_info := LocationInfo file_0 41 2 53 3.
+  Definition loc_31 : location_info := LocationInfo file_0 41 27 43 3.
+  Definition loc_32 : location_info := LocationInfo file_0 42 4 42 26.
+  Definition loc_33 : location_info := LocationInfo file_0 42 11 42 25.
+  Definition loc_34 : location_info := LocationInfo file_0 43 9 53 3.
+  Definition loc_35 : location_info := LocationInfo file_0 44 4 44 48.
+  Definition loc_36 : location_info := LocationInfo file_0 45 4 45 21.
+  Definition loc_37 : location_info := LocationInfo file_0 46 4 52 5.
+  Definition loc_38 : location_info := LocationInfo file_0 46 27 50 5.
+  Definition loc_39 : location_info := LocationInfo file_0 47 6 47 22.
+  Definition loc_40 : location_info := LocationInfo file_0 48 6 48 24.
+  Definition loc_41 : location_info := LocationInfo file_0 49 6 49 18.
+  Definition loc_42 : location_info := LocationInfo file_0 49 13 49 17.
+  Definition loc_43 : location_info := LocationInfo file_0 49 13 49 17.
+  Definition loc_44 : location_info := LocationInfo file_0 48 6 48 16.
+  Definition loc_45 : location_info := LocationInfo file_0 48 6 48 10.
+  Definition loc_46 : location_info := LocationInfo file_0 48 6 48 10.
+  Definition loc_47 : location_info := LocationInfo file_0 48 19 48 23.
+  Definition loc_48 : location_info := LocationInfo file_0 48 19 48 23.
+  Definition loc_49 : location_info := LocationInfo file_0 47 6 47 8.
+  Definition loc_50 : location_info := LocationInfo file_0 47 7 47 8.
+  Definition loc_51 : location_info := LocationInfo file_0 47 7 47 8.
+  Definition loc_52 : location_info := LocationInfo file_0 47 11 47 21.
+  Definition loc_53 : location_info := LocationInfo file_0 47 11 47 21.
+  Definition loc_54 : location_info := LocationInfo file_0 47 11 47 15.
+  Definition loc_55 : location_info := LocationInfo file_0 47 11 47 15.
+  Definition loc_56 : location_info := LocationInfo file_0 47 13 47 14.
+  Definition loc_57 : location_info := LocationInfo file_0 47 13 47 14.
+  Definition loc_58 : location_info := LocationInfo file_0 50 11 52 5.
+  Definition loc_59 : location_info := LocationInfo file_0 51 6 51 18.
+  Definition loc_60 : location_info := LocationInfo file_0 51 13 51 17.
+  Definition loc_61 : location_info := LocationInfo file_0 51 13 51 17.
+  Definition loc_62 : location_info := LocationInfo file_0 46 7 46 25.
+  Definition loc_63 : location_info := LocationInfo file_0 46 7 46 12.
+  Definition loc_64 : location_info := LocationInfo file_0 46 7 46 12.
+  Definition loc_65 : location_info := LocationInfo file_0 46 16 46 25.
+  Definition loc_66 : location_info := LocationInfo file_0 46 16 46 25.
+  Definition loc_67 : location_info := LocationInfo file_0 46 16 46 20.
+  Definition loc_68 : location_info := LocationInfo file_0 46 16 46 20.
+  Definition loc_69 : location_info := LocationInfo file_0 46 18 46 19.
+  Definition loc_70 : location_info := LocationInfo file_0 46 18 46 19.
+  Definition loc_71 : location_info := LocationInfo file_0 45 18 45 20.
+  Definition loc_72 : location_info := LocationInfo file_0 45 18 45 20.
+  Definition loc_73 : location_info := LocationInfo file_0 45 19 45 20.
+  Definition loc_74 : location_info := LocationInfo file_0 45 19 45 20.
+  Definition loc_77 : location_info := LocationInfo file_0 44 18 44 47.
+  Definition loc_78 : location_info := LocationInfo file_0 44 18 44 27.
+  Definition loc_79 : location_info := LocationInfo file_0 44 18 44 27.
+  Definition loc_80 : location_info := LocationInfo file_0 44 28 44 39.
+  Definition loc_81 : location_info := LocationInfo file_0 44 29 44 39.
+  Definition loc_82 : location_info := LocationInfo file_0 44 29 44 33.
+  Definition loc_83 : location_info := LocationInfo file_0 44 29 44 33.
+  Definition loc_84 : location_info := LocationInfo file_0 44 31 44 32.
+  Definition loc_85 : location_info := LocationInfo file_0 44 31 44 32.
+  Definition loc_86 : location_info := LocationInfo file_0 44 41 44 46.
+  Definition loc_87 : location_info := LocationInfo file_0 44 41 44 46.
+  Definition loc_90 : location_info := LocationInfo file_0 41 5 41 25.
+  Definition loc_91 : location_info := LocationInfo file_0 41 5 41 7.
+  Definition loc_92 : location_info := LocationInfo file_0 41 5 41 7.
+  Definition loc_93 : location_info := LocationInfo file_0 41 6 41 7.
+  Definition loc_94 : location_info := LocationInfo file_0 41 6 41 7.
+  Definition loc_95 : location_info := LocationInfo file_0 41 11 41 25.
+  Definition loc_98 : location_info := LocationInfo file_0 63 2 71 3.
+  Definition loc_99 : location_info := LocationInfo file_0 63 27 65 3.
+  Definition loc_100 : location_info := LocationInfo file_0 64 4 64 11.
+  Definition loc_102 : location_info := LocationInfo file_0 65 9 71 3.
+  Definition loc_103 : location_info := LocationInfo file_0 66 4 66 26.
+  Definition loc_104 : location_info := LocationInfo file_0 67 4 67 40.
+  Definition loc_105 : location_info := LocationInfo file_0 68 4 68 23.
+  Definition loc_106 : location_info := LocationInfo file_0 69 4 69 17.
+  Definition loc_107 : location_info := LocationInfo file_0 70 4 70 22.
+  Definition loc_108 : location_info := LocationInfo file_0 70 4 70 10.
+  Definition loc_109 : location_info := LocationInfo file_0 70 4 70 10.
+  Definition loc_110 : location_info := LocationInfo file_0 70 11 70 12.
+  Definition loc_111 : location_info := LocationInfo file_0 70 11 70 12.
+  Definition loc_112 : location_info := LocationInfo file_0 70 14 70 20.
+  Definition loc_113 : location_info := LocationInfo file_0 70 14 70 20.
+  Definition loc_114 : location_info := LocationInfo file_0 69 4 69 13.
+  Definition loc_115 : location_info := LocationInfo file_0 69 4 69 13.
+  Definition loc_116 : location_info := LocationInfo file_0 69 14 69 15.
+  Definition loc_117 : location_info := LocationInfo file_0 69 14 69 15.
+  Definition loc_118 : location_info := LocationInfo file_0 68 4 68 13.
+  Definition loc_119 : location_info := LocationInfo file_0 68 4 68 13.
+  Definition loc_120 : location_info := LocationInfo file_0 68 14 68 21.
+  Definition loc_121 : location_info := LocationInfo file_0 68 15 68 21.
+  Definition loc_122 : location_info := LocationInfo file_0 67 20 67 39.
+  Definition loc_123 : location_info := LocationInfo file_0 67 20 67 29.
+  Definition loc_124 : location_info := LocationInfo file_0 67 20 67 29.
+  Definition loc_125 : location_info := LocationInfo file_0 67 30 67 31.
+  Definition loc_126 : location_info := LocationInfo file_0 67 30 67 31.
+  Definition loc_127 : location_info := LocationInfo file_0 67 33 67 38.
+  Definition loc_128 : location_info := LocationInfo file_0 67 33 67 38.
+  Definition loc_131 : location_info := LocationInfo file_0 66 16 66 25.
+  Definition loc_132 : location_info := LocationInfo file_0 66 16 66 25.
+  Definition loc_133 : location_info := LocationInfo file_0 66 16 66 20.
+  Definition loc_134 : location_info := LocationInfo file_0 66 16 66 20.
+  Definition loc_135 : location_info := LocationInfo file_0 66 18 66 19.
+  Definition loc_136 : location_info := LocationInfo file_0 66 18 66 19.
+  Definition loc_139 : location_info := LocationInfo file_0 63 5 63 25.
+  Definition loc_140 : location_info := LocationInfo file_0 63 5 63 7.
+  Definition loc_141 : location_info := LocationInfo file_0 63 5 63 7.
+  Definition loc_142 : location_info := LocationInfo file_0 63 6 63 7.
+  Definition loc_143 : location_info := LocationInfo file_0 63 6 63 7.
+  Definition loc_144 : location_info := LocationInfo file_0 63 11 63 25.
 
   (* Definition of struct [list_node]. *)
   Program Definition struct_list_node := {|
@@ -176,7 +218,7 @@ Section code.
         "head" <-{ LPtr }
           LocInfoE loc_71 (use{LPtr} (LocInfoE loc_73 (!{LPtr} (LocInfoE loc_74 ("l"))))) ;
         locinfo: loc_62 ;
-        if: LocInfoE loc_62 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_62 ((LocInfoE loc_63 (use{it_layout i32} (LocInfoE loc_64 ((LocInfoE loc_65 (!{LPtr} (LocInfoE loc_67 (!{LPtr} (LocInfoE loc_68 ("l")))))) at{struct_list_node} "val")))) ≤{IntOp i32, IntOp i32} (LocInfoE loc_69 (use{it_layout i32} (LocInfoE loc_70 ("pivot")))))))
+        if: LocInfoE loc_62 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_62 ((LocInfoE loc_63 (use{it_layout i32} (LocInfoE loc_64 ("pivot")))) ≤{IntOp i32, IntOp i32} (LocInfoE loc_65 (use{it_layout i32} (LocInfoE loc_66 ((LocInfoE loc_67 (!{LPtr} (LocInfoE loc_69 (!{LPtr} (LocInfoE loc_70 ("l")))))) at{struct_list_node} "val")))))))
         then
         locinfo: loc_39 ;
           Goto "#3"
@@ -200,4 +242,51 @@ Section code.
       ]> $∅
     )%E
   |}.
+
+  (* Definition of function [quicksort]. *)
+  Definition impl_quicksort (append partition quicksort : loc): function := {|
+    f_args := [
+      ("l", LPtr)
+    ];
+    f_local_vars := [
+      ("pivot", it_layout i32);
+      ("higher", LPtr)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_139 ;
+        if: LocInfoE loc_139 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_139 ((LocInfoE loc_140 (use{LPtr} (LocInfoE loc_142 (!{LPtr} (LocInfoE loc_143 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_144 (NULL)))))
+        then
+        locinfo: loc_100 ;
+          Goto "#1"
+        else
+        Goto "#2"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_100 ;
+        Return (VOID)
+      ]> $
+      <[ "#2" :=
+        "pivot" <-{ it_layout i32 }
+          LocInfoE loc_131 (use{it_layout i32} (LocInfoE loc_132 ((LocInfoE loc_133 (!{LPtr} (LocInfoE loc_135 (!{LPtr} (LocInfoE loc_136 ("l")))))) at{struct_list_node} "val"))) ;
+        locinfo: loc_122 ;
+        "$0" <- LocInfoE loc_124 (partition) with
+          [ LocInfoE loc_125 (use{LPtr} (LocInfoE loc_126 ("l"))) ;
+          LocInfoE loc_127 (use{it_layout i32} (LocInfoE loc_128 ("pivot"))) ] ;
+        "higher" <-{ LPtr } LocInfoE loc_122 ("$0") ;
+        locinfo: loc_105 ;
+        "_" <- LocInfoE loc_119 (quicksort) with
+          [ LocInfoE loc_120 (&(LocInfoE loc_121 ("higher"))) ] ;
+        locinfo: loc_106 ;
+        "_" <- LocInfoE loc_115 (quicksort) with
+          [ LocInfoE loc_116 (use{LPtr} (LocInfoE loc_117 ("l"))) ] ;
+        locinfo: loc_107 ;
+        "_" <- LocInfoE loc_109 (append) with
+          [ LocInfoE loc_110 (use{LPtr} (LocInfoE loc_111 ("l"))) ;
+          LocInfoE loc_112 (use{LPtr} (LocInfoE loc_113 ("higher"))) ] ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
 End code.
diff --git a/tutorial/proofs/quicksort_solution/generated_proof_append.v b/tutorial/proofs/quicksort_solution/generated_proof_append.v
index f94b8060..478e520e 100644
--- a/tutorial/proofs/quicksort_solution/generated_proof_append.v
+++ b/tutorial/proofs/quicksort_solution/generated_proof_append.v
@@ -1,6 +1,7 @@
 From refinedc.typing Require Import typing.
 From refinedc.tutorial.quicksort_solution Require Import generated_code.
 From refinedc.tutorial.quicksort_solution Require Import generated_spec.
+From refinedc.tutorial.quicksort_solution Require Import list_proofs.
 Set Default Proof Using "Type".
 
 (* Generated from [tutorial/quicksort_solution.c]. *)
diff --git a/tutorial/proofs/quicksort_solution/generated_proof_partition.v b/tutorial/proofs/quicksort_solution/generated_proof_partition.v
index 5e38bede..cb59b8a9 100644
--- a/tutorial/proofs/quicksort_solution/generated_proof_partition.v
+++ b/tutorial/proofs/quicksort_solution/generated_proof_partition.v
@@ -1,6 +1,7 @@
 From refinedc.typing Require Import typing.
 From refinedc.tutorial.quicksort_solution Require Import generated_code.
 From refinedc.tutorial.quicksort_solution Require Import generated_spec.
+From refinedc.tutorial.quicksort_solution Require Import list_proofs.
 Set Default Proof Using "Type".
 
 (* Generated from [tutorial/quicksort_solution.c]. *)
diff --git a/tutorial/proofs/quicksort_solution/generated_proof_quicksort.v b/tutorial/proofs/quicksort_solution/generated_proof_quicksort.v
new file mode 100644
index 00000000..919065e8
--- /dev/null
+++ b/tutorial/proofs/quicksort_solution/generated_proof_quicksort.v
@@ -0,0 +1,31 @@
+From refinedc.typing Require Import typing.
+From refinedc.tutorial.quicksort_solution Require Import generated_code.
+From refinedc.tutorial.quicksort_solution Require Import generated_spec.
+From refinedc.tutorial.quicksort_solution Require Import list_proofs.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/quicksort_solution.c]. *)
+Section proof_quicksort.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [quicksort]. *)
+  Lemma type_quicksort (append partition quicksort : loc) :
+    append ◁ᵥ append @ function_ptr type_of_append -∗
+    partition ◁ᵥ partition @ function_ptr type_of_partition -∗
+    quicksort ◁ᵥ quicksort @ function_ptr type_of_quicksort -∗
+    typed_function (impl_quicksort append partition quicksort) type_of_quicksort.
+  Proof.
+    start_function "quicksort" ([list_l l]) => arg_l local_pivot local_higher.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "quicksort" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: try (eapply sorted_append_middle_el => //; [ apply _ | | ]; last first).
+    all: repeat list_perm_subst; eauto using filter_permutation, Forall_filter with lia.
+    all: print_sidecondition_goal "quicksort".
+  Qed.
+End proof_quicksort.
diff --git a/tutorial/proofs/quicksort_solution/generated_spec.v b/tutorial/proofs/quicksort_solution/generated_spec.v
index 75122596..f83f52d2 100644
--- a/tutorial/proofs/quicksort_solution/generated_spec.v
+++ b/tutorial/proofs/quicksort_solution/generated_spec.v
@@ -1,5 +1,6 @@
 From refinedc.typing Require Import typing.
 From refinedc.tutorial.quicksort_solution Require Import generated_code.
+From refinedc.tutorial.quicksort_solution Require Import list_proofs.
 Set Default Proof Using "Type".
 
 (* Generated from [tutorial/quicksort_solution.c]. *)
@@ -75,7 +76,12 @@ Section spec.
   (* Specifications for function [partition]. *)
   Definition type_of_partition :=
     fn(∀ (p, xs, z) : loc * (list Z) * Z; (p @ (&own (xs @ (list_t)))), (z @ (int (i32))); True)
-      → ∃ () : (), ((filter (λ v, v <= z) xs) @ (list_t)); (p ◁ₗ ((filter (λ v, v > z) xs) @ (list_t))).
+      → ∃ () : (), ((filter (λ v, z <= v) xs) @ (list_t)); (p ◁ₗ ((filter (λ v, v < z) xs) @ (list_t))).
+
+  (* Specifications for function [quicksort]. *)
+  Definition type_of_quicksort :=
+    fn(∀ (list_l, l) : (list Z) * loc; (l @ (&own (list_l @ (list_t)))); True)
+      → ∃ sorted_l : (list Z), (void); (l ◁ₗ (sorted_l @ (list_t))) ∗ ⌜Permutation list_l sorted_l⌝ ∗ ⌜Sorted Z.le sorted_l⌝.
 End spec.
 
 Typeclasses Opaque list_t_rec.
diff --git a/tutorial/proofs/quicksort_solution/list_proofs.v b/tutorial/proofs/quicksort_solution/list_proofs.v
new file mode 100644
index 00000000..2eeada83
--- /dev/null
+++ b/tutorial/proofs/quicksort_solution/list_proofs.v
@@ -0,0 +1,66 @@
+From refinedc.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section filter_proof.
+  Context {A : Type}.
+  Implicit Types (P : A → Prop).
+
+  Lemma filter_permutation xs P P' `{∀ x, Decision (P' x), ∀ x, Decision (P x)}: 
+    (∀ x, ¬ P x ↔ P' x) →
+    xs ≡ₚ filter P xs ++ filter P' xs.
+  Proof.
+    move => HPP'.
+    induction xs as [|a xs IHxs] => //.
+    rewrite !filter_cons.
+    destruct (decide (P a)) as [HP | HnP].
+    + rewrite decide_False; [ | contradict HP; by apply HPP'].
+      apply perm_skip, IHxs.
+    + rewrite decide_True; [ | by apply HPP'].
+      rewrite -Permutation_middle.
+      apply perm_skip, IHxs.
+  Qed.
+
+  Lemma Forall_filter xs P P' `{∀ x, Decision (P' x)} :
+    (∀ x, P' x → P x) →
+    Forall P (filter P' xs).
+  Proof.
+    move => HPP'.
+    induction xs as [|a xs IHxs].
+    + by rewrite filter_nil.
+    + rewrite filter_cons.
+      destruct (decide _) => //.
+      apply Forall_cons; split => //.
+      by apply HPP'.
+  Qed.
+
+End filter_proof.
+
+Section sorted_list_proof.
+  Context {A : Type}.
+  Context (R : A → A → Prop).
+
+  Lemma sorted_append_middle_el xs ys m:
+    Transitive R →
+    Sorted R xs →
+    Sorted R ys →
+    Forall (λ e, R e m) xs →
+    Forall (λ e, R m e) ys →
+    Sorted R (xs ++ ys).
+  Proof.
+    move => H /Sorted_StronglySorted H1 /Sorted_StronglySorted H2 Hxs Hys.
+    apply StronglySorted_Sorted.
+    induction xs as [|a xs IHxs] => //=.
+    inversion Hxs. apply SSorted_cons.
+    + apply: IHxs => //.
+      by eapply StronglySorted_inv.
+    + apply Forall_app_2; first by apply StronglySorted_inv.
+      eapply Forall_impl => //= x3.
+      by apply H.
+  Qed.
+
+End sorted_list_proof.
+
+Ltac list_perm_subst := 
+  match goal with 
+  | H: ?listL ≡ₚ ?listR |- ?P => (rewrite H => {H} || rewrite -H => {H})
+  end.
diff --git a/tutorial/proofs/quicksort_solution/proof_files b/tutorial/proofs/quicksort_solution/proof_files
index 0b5500e1..97f3be09 100644
--- a/tutorial/proofs/quicksort_solution/proof_files
+++ b/tutorial/proofs/quicksort_solution/proof_files
@@ -1,2 +1,3 @@
 generated_proof_append.v
 generated_proof_partition.v
+generated_proof_quicksort.v
diff --git a/tutorial/quicksort_exercise.c b/tutorial/quicksort_exercise.c
index cf41841a..1ee5e524 100644
--- a/tutorial/quicksort_exercise.c
+++ b/tutorial/quicksort_exercise.c
@@ -32,7 +32,7 @@ list_t partition(list_t *l, int pivot) {
   } else {
     list_t rest = partition(&(*l)->next, pivot);
     list_t head = *l;
-    if((*l)->val <= pivot) {
+    if(pivot <= (*l)->val) {
       *l = (*l)->next;
       head->next = rest;
       return head;
@@ -41,3 +41,15 @@ list_t partition(list_t *l, int pivot) {
     }
   }
 }
+
+void quicksort(list_t* l) {
+  if(*l == NULL) {
+    return;
+  } else {
+    int pivot = (*l)->val;
+    list_t higher = partition(l, pivot);
+    quicksort(&higher);
+    quicksort(l);
+    append(l, higher);
+  }
+}
diff --git a/tutorial/quicksort_solution.c b/tutorial/quicksort_solution.c
index 6b3918f1..65c848de 100644
--- a/tutorial/quicksort_solution.c
+++ b/tutorial/quicksort_solution.c
@@ -1,5 +1,7 @@
 #include <stddef.h>
 
+//@rc::import list_proofs from refinedc.tutorial.quicksort_solution
+
 typedef struct
   [[rc::refined_by("xs : {list Z}")]]
   [[rc::ptr_type("list_t : {xs <> []} @ optional<&own<...>, null>")]]
@@ -32,8 +34,8 @@ void append(list_t *l, list_t k) {
 
 [[rc::parameters("p : loc", "xs : {list Z}", "z : Z")]]
 [[rc::args("p @ &own<xs @ list_t>", "z @ int<i32>")]]
-[[rc::returns("{filter (λ v, v <= z) xs} @ list_t")]]
-[[rc::ensures("p @ &own<{filter (λ v, v > z) xs} @ list_t>")]]
+[[rc::returns("{filter (λ v, z <= v) xs} @ list_t")]]
+[[rc::ensures("p @ &own<{filter (λ v, v < z) xs} @ list_t>")]]
 [[rc::tactics("all: try by rewrite filter_cons; solve_goal.")]]
 list_t partition(list_t *l, int pivot) {
   if(*l == NULL) {
@@ -41,7 +43,7 @@ list_t partition(list_t *l, int pivot) {
   } else {
     list_t rest = partition(&(*l)->next, pivot);
     list_t head = *l;
-    if((*l)->val <= pivot) {
+    if(pivot <= (*l)->val) {
       *l = (*l)->next;
       head->next = rest;
       return head;
@@ -51,4 +53,20 @@ list_t partition(list_t *l, int pivot) {
   }
 }
 
-// TODO: quicksort
+[[rc::parameters  ("list_l : {list Z}", "l : loc")]]
+[[rc::args        ("l @ &own<list_l @ list_t>")]]
+[[rc::exists      ("sorted_l : {list Z}")]]
+[[rc::ensures     ("l @ &own<sorted_l @ list_t>", "{Permutation list_l sorted_l}", "{Sorted Z.le sorted_l}")]]
+[[rc::tactics     ("all: try (eapply sorted_append_middle_el => //; [ apply _ | | ]; last first).")]]
+[[rc::tactics     ("all: repeat list_perm_subst; eauto using filter_permutation, Forall_filter with lia.")]]
+void quicksort(list_t* l) {
+  if(*l == NULL) {
+    return;
+  } else {
+    int pivot = (*l)->val;
+    list_t higher = partition(l, pivot);
+    quicksort(&higher);
+    quicksort(l);
+    append(l, higher);
+  }
+}
-- 
GitLab