Add SimplExist and SimplForall

frontend/coq_pp.ml

@@ -1288,7 +1288,13 @@ let pp_proof : Coq_path.t -> func_def -> import list -> string list
       List.iter (fun (x,_) -> pp " arg_%s" x) def.func_args;
       List.iter (fun (x,_) -> pp " local_%s" x) def.func_vars
     end;
-  pp ".@;split_blocks ((";
+  pp ".@;";
+  if func_annot.fa_parameters <> [] then
+    begin
+      let pp_var ff (x, _) = pp_print_string ff x in
+      pp "prepare_parameters (%a).@;" (pp_sep " " pp_var) func_annot.fa_parameters;
+    end;
+  pp "split_blocks ((";
   let pp_inv (id, annot) =
     (* Opening a box and printing the existentials. *)
     pp "@;  @[<v 2><[ \"%s\" :=" id;

linux/casestudies/proofs/pgtable/pgtable_lemmas.v

@@ -53,6 +53,30 @@ Global Instance Pte_BitfieldDesc : BitfieldDesc Pte := {|
   bitfield_repr := pte_repr;
   bitfield_wf := pte_wf;
 |}.
+(*
+Global Instance simpl_exist_Pte P : SimplExist Pte P
+   (∃ valid type leaf_attr_lo addr undef leaf_attr_hi,
+       P {|
+           pte_valid := valid;
+           pte_type := type;
+           pte_leaf_attr_lo := leaf_attr_lo;
+           pte_addr := addr;
+           pte_undef := undef;
+           pte_leaf_attr_hi := leaf_attr_hi;
+         |}).
+Proof. unfold SimplExist. naive_solver. Qed.
+Global Instance simpl_forall_Pte P : SimplForall Pte 6 P
+   (∀ valid type leaf_attr_lo addr undef leaf_attr_hi,
+       P {|
+           pte_valid := valid;
+           pte_type := type;
+           pte_leaf_attr_lo := leaf_attr_lo;
+           pte_addr := addr;
+           pte_undef := undef;
+           pte_leaf_attr_hi := leaf_attr_hi;
+         |}).
+Proof. unfold SimplForall => ? []. naive_solver. Qed.
+ *)
 
 Definition addr_of (n : Z) : Z :=
   bf_slice 12 36 n.
@@ -119,6 +143,10 @@ Global Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
   bitfield_repr := prot_repr;
   bitfield_wf := prot_wf;
 |}.
+Global Instance simpl_exist_Prot P : SimplExist Prot P (∃ x w r device, P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
+Proof. unfold SimplExist. naive_solver. Qed.
+Global Instance simpl_forall_Prot P : SimplForall Prot 4 P (∀ x w r device, P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
+Proof. unfold SimplForall => ? []. naive_solver. Qed.
 
 (* struct, const *)
 

theories/lithium/interpreter.v

@@ -501,7 +501,7 @@ Ltac liExist protect :=
   | _ => idtac
   end;
   lazymatch goal with
-  | |- @ex ?A _ =>
+  | |- @ex ?A ?P =>
     first [
         custom_exist_tac A protect
       | lazymatch A with
@@ -512,10 +512,15 @@ Ltac liExist protect :=
         | sigT _ => apply: tac_exist_sigT
         | unit => exists tt
         | ?A =>
+            first [
+                let p := constr:(_ : SimplExist A P _) in
+                refine (@simpl_exist_proof _ _ _ p _)
+              |
                 lazymatch protect with
                 | true => let Hevar := create_protected_evar A in exists (protected Hevar)
                 | false => eexists _
                 end
+              ]
         end ]
   | _ => fail "do_exist: unknown goal"
   end.
@@ -595,26 +600,46 @@ Ltac liImpl :=
   end.
 
 Ltac liForall :=
-  let do_intro name :=
-    repeat lazymatch goal with
+  (* n tells us how many quantifiers we should introduce with this name *)
+  let rec do_intro n name :=
+    lazymatch n with
+    | S ?n' =>
+      lazymatch goal with
       (* relying on the fact that unification variables cannot contain
          dependent variables to distinguish between dependent and non dependent forall *)
-    | |- ?P -> ?Q => fail "implication, not forall"
-    | |- forall _ : ?P, _ =>
+      | |- ?P -> ?Q =>
+          lazymatch type of P with
+          | Prop => fail "implication, not forall"
+          | _ => (* just some unused variable, discard *) move => _
+          end
+      | |- forall _ : ?A, _ =>
         (* When changing this, also change [prepare_initial_coq_context] in automation.v *)
-      lazymatch P with
-      | (prod _ _) => case
+        lazymatch A with
+        | (prod _ _) => case; do_intro (S (S O)) name
         | unit => case
-      | _ => let H := fresh name in intro H
+        | _ =>
+            first [
+                (* We match again since having e in the context when calling fresh can mess up names. *)
+                lazymatch goal with
+                | |- forall e : ?A, @?P e =>
+                    let sn := open_constr:(_ : nat) in
+                    let p := constr:(_ : SimplForall A sn P _) in
+                    refine (@simpl_forall_proof _ _ _ _ p _);
+                    do_intro sn name
+                end
+              | let H := fresh name in intro H
+              ]
         end
+      end; do_intro n' name
+    | O => idtac
     end
   in
   lazymatch goal with
-  | |- envs_entails _ (bi_forall (λ name, _)) => notypeclasses refine (tac_do_forall _ _ _ _); do_intro name
+  | |- envs_entails _ (bi_forall (λ name, _)) => notypeclasses refine (tac_do_forall _ _ _ _); do_intro (S O) name
   | |- envs_entails _ (bi_wand (bi_exist (λ name, _)) _) =>
-    notypeclasses refine (tac_do_exist_wand _ _ _ _ _); do_intro name
-  | |- (∃ name, _) → _ => case; do_intro name
-  | |- forall name, _ => do_intro name
+    notypeclasses refine (tac_do_exist_wand _ _ _ _ _); do_intro (S O) name
+  | |- (∃ name, _) → _ => case; do_intro (S O) name
+  | |- forall name, _ => do_intro (S O) name
   | _ => fail "do_forall: unknown goal"
   end.
 

theories/lithium/simpl_classes.v

 From refinedc.lithium Require Import base.
 
+Class SimplExist (T : Type) (e : T → Prop) (Q: Prop) := simpl_exist_proof : Q → ∃ x, e x.
+Class SimplForall (T : Type) (n : nat) (e : T → Prop) (Q: Prop) := simpl_forall_proof : Q → ∀ x, e x.
+
 Class SimplImplUnsafe (changed : bool) (P : Prop) (Ps : Prop → Prop) := simpl_impl_unsafe T: (Ps T) → (P → T).
 Class SimplAndUnsafe (changed : bool) (P : Prop) (Ps : Prop → Prop) := simpl_and_unsafe T: (Ps T) → (P ∧ T).
 Global Instance simplimpl_unsafe_id (P : Prop) : SimplImplUnsafe false P (λ T, P → T) | 1000.

theories/typing/automation.v

@@ -278,25 +278,6 @@ Tactic Notation "liRStepUntil" open_constr(id) :=
 
 
 (** * Tactics for starting a function *)
-(* Recursively destruct a product in hypothesis H, using the given name as template. *)
-Ltac destruct_product_hypothesis name H :=
-  match goal with
-  | H : _ * _ |- _ => let tmp1 := fresh "tmp" in
-                      let tmp2 := fresh "tmp" in
-                      destruct H as [tmp1 tmp2];
-                      destruct_product_hypothesis name tmp1;
-                      destruct_product_hypothesis name tmp2
-  |           |- _ => let id := fresh name in
-                      rename H into id
-  end.
-
-Ltac prepare_initial_coq_context :=
-  (* The automation assumes that all products in the context are destructed, see liForall *)
-  repeat lazymatch goal with
-  | H : _ * _ |- _ => destruct_product_hypothesis H H
-  | H : unit |- _ => destruct H
-  end.
-
 (* IMPORTANT: We need to make sure to never call simpl while the code
 (Q) is part of the goal, because simpl seems to take exponential time
 in the number of blocks! *)
@@ -308,7 +289,10 @@ Tactic Notation "start_function" constr(fnname) "(" simple_intropattern(x) ")" :
   iIntros ( x );
   iSplit; [iPureIntro; simpl; by [repeat constructor] || fail "in" fnname "argument types don't match layout of arguments" |];
   let lsa := fresh "lsa" in let lsv := fresh "lsv" in
-  iIntros "!#" (lsa lsv); inv_vec lsv; inv_vec lsa; prepare_initial_coq_context.
+  iIntros "!#" (lsa lsv); inv_vec lsv; inv_vec lsa.
+
+Tactic Notation "prepare_parameters" "(" ident_list(i) ")" :=
+  revert i; repeat liForall.
 
 Ltac liRSplitBlocksIntro :=
   repeat (