clean admits in pgtable_lemmas.v

linux/casestudies/proofs/pgtable/pgtable_lemmas.v

@@ -43,12 +43,14 @@ Global Instance Pte_S1_attr_lo_sig_wf : SigWf Pte_S1_attr_lo_sig.
 Proof. solve_sig_wf. Qed.
 
 Global Instance Pte_S1_attr_lo_tm_value r :
-  SimplAnd (IsValue (Pte_S1_attr_lo_tm r)) (λ T, T).
-Admitted.
+  IsValue (Pte_S1_attr_lo_tm r).
+Proof. repeat constructor. Qed.
 
 Global Instance Pte_S1_attr_lo_tm_sort r `{!CanSolve (Pte_S1_attr_lo_wf r)} :
-  SimplAnd (HasSort (Pte_S1_attr_lo_tm r) Pte_S1_attr_lo_sig) (λ T, T).
-Admitted.
+  HasSort (Pte_S1_attr_lo_tm r) Pte_S1_attr_lo_sig.
+Proof.
+  unfold HasSort; solve_goal.
+Qed.
 
 Record Pte_S1_attr_hi := {
   attr_hi_s1_xn : bool;
@@ -75,12 +77,14 @@ Global Instance Pte_S1_attr_hi_sig_wf : SigWf Pte_S1_attr_hi_sig.
 Proof. solve_sig_wf. Qed.
 
 Global Instance Pte_S1_attr_hi_tm_value r :
-  SimplAnd (IsValue (Pte_S1_attr_hi_tm r)) (λ T, T).
-Admitted.
+  IsValue (Pte_S1_attr_hi_tm r).
+Proof. repeat constructor. Qed.
 
 Global Instance Pte_S1_attr_hi_tm_sort r `{!CanSolve (Pte_S1_attr_hi_wf r)} :
-  SimplAnd (HasSort (Pte_S1_attr_hi_tm r) Pte_S1_attr_hi_sig) (λ T, T).
-Admitted.
+  HasSort (Pte_S1_attr_hi_tm r) Pte_S1_attr_hi_sig.
+Proof.
+  unfold HasSort; solve_goal.
+Qed.
 
 (* S2 specific *)
 
@@ -129,12 +133,14 @@ Global Instance Pte_S2_attr_lo_sig_wf : SigWf Pte_S2_attr_lo_sig.
 Proof. solve_sig_wf. Qed.
 
 Global Instance Pte_S2_attr_lo_tm_value r :
-  SimplAnd (IsValue (Pte_S2_attr_lo_tm r)) (λ T, T).
-Admitted.
+  IsValue (Pte_S2_attr_lo_tm r).
+Proof. repeat constructor. Qed.
 
 Global Instance Pte_S2_attr_lo_tm_sort r `{!CanSolve (Pte_S2_attr_lo_wf r)} :
-  SimplAnd (HasSort (Pte_S2_attr_lo_tm r) Pte_S2_attr_lo_sig) (λ T, T).
-Admitted.
+  HasSort (Pte_S2_attr_lo_tm r) Pte_S2_attr_lo_sig.
+Proof.
+  unfold HasSort; solve_goal.
+Qed.
 
 Record Pte_S2_attr_hi := {
   attr_hi_s2_xn : bool;
@@ -161,12 +167,14 @@ Global Instance Pte_S2_attr_hi_sig_wf : SigWf Pte_S2_attr_hi_sig.
 Proof. solve_sig_wf. Qed.
 
 Global Instance Pte_S2_attr_hi_tm_value r :
-  SimplAnd (IsValue (Pte_S2_attr_hi_tm r)) (λ T, T).
-Admitted.
+  IsValue (Pte_S2_attr_hi_tm r).
+Proof. repeat constructor. Qed.
 
 Global Instance Pte_S2_attr_hi_tm_sort r `{!CanSolve (Pte_S2_attr_hi_wf r)} :
-  SimplAnd (HasSort (Pte_S2_attr_hi_tm r) Pte_S2_attr_hi_sig) (λ T, T).
-Admitted.
+  HasSort (Pte_S2_attr_hi_tm r) Pte_S2_attr_hi_sig.
+Proof.
+  unfold HasSort; solve_goal.
+Qed.
 
 (* Pte *)
 
@@ -256,34 +264,46 @@ Global Program Instance Pte_bd : BitfieldDesc Pte := {|
 |}.
 
 Global Instance Pte_attr_lo_tm_value r :
-  SimplAnd (IsValue (sum_elim r Pte_S1_attr_lo_tm Pte_S2_attr_lo_tm))
-    (λ T, T).
-Admitted.
-
-Global Instance Pte_attr_lo_tm_sort r s `{!CanSolve (sum_elim r Pte_S1_attr_lo_wf
-       Pte_S2_attr_lo_wf)} :
-  SimplAnd (HasSort
-    (sum_elim r Pte_S1_attr_lo_tm Pte_S2_attr_lo_tm)
-    match s with
+  IsValue (sum_elim r Pte_S1_attr_lo_tm Pte_S2_attr_lo_tm).
+Proof.
+  destruct r; typeclasses eauto.
+Qed.
+
+Global Instance Pte_attr_lo_tm_sort r s
+  `{!CanSolve (sum_elim r Pte_S1_attr_lo_wf Pte_S2_attr_lo_wf)}
+  `{!CanSolve (match s with
+                | S1 => (∃ a, r = inl a)
+                | S2 => (∃ a, r = inr a)
+               end)}:
+  HasSort (sum_elim r Pte_S1_attr_lo_tm Pte_S2_attr_lo_tm)
+    (match s with
     | S1 => Pte_S1_attr_lo_sig
     | S2 => Pte_S2_attr_lo_sig
-    end) (λ T, T).
-Admitted.
+    end).
+Proof.
+  unfold CanSolve in *; case_match; destruct CanSolve1; subst; typeclasses eauto.
+Qed.
 
 Global Instance Pte_attr_hi_tm_value r :
-  SimplAnd (IsValue (sum_elim r Pte_S1_attr_hi_tm Pte_S2_attr_hi_tm))
-    (λ T, T).
-Admitted.
-
-Global Instance Pte_attr_hi_tm_sort r s `{!CanSolve (sum_elim r Pte_S1_attr_hi_wf
-       Pte_S2_attr_hi_wf)} :
-  SimplAnd (HasSort
-    (sum_elim r Pte_S1_attr_hi_tm Pte_S2_attr_hi_tm)
-    match s with
+  IsValue (sum_elim r Pte_S1_attr_hi_tm Pte_S2_attr_hi_tm).
+Proof.
+  destruct r; typeclasses eauto.
+Qed.
+
+Global Instance Pte_attr_hi_tm_sort r s
+  `{!CanSolve (sum_elim r Pte_S1_attr_hi_wf Pte_S2_attr_hi_wf)}
+  `{!CanSolve (match s with
+                | S1 => (∃ a, r = inl a)
+                | S2 => (∃ a, r = inr a)
+               end)} :
+  HasSort (sum_elim r Pte_S1_attr_hi_tm Pte_S2_attr_hi_tm)
+    (match s with
     | S1 => Pte_S1_attr_hi_sig
     | S2 => Pte_S2_attr_hi_sig
-    end) (λ T, T).
-Admitted.
+    end).
+Proof.
+  unfold CanSolve in *; case_match; destruct CanSolve1; subst; typeclasses eauto.
+Qed.
 
 Global Instance simple_protected_Pte_constraints p `{!IsProtected p} x r `{!CanSolve (Pte_constraints x r)} :
   SimplAndUnsafe true (Pte_constraints p r) (λ T, p = x ∧ T).

theories/lang/bitfield.v

@@ -166,6 +166,14 @@ Proof.
   split; naive_solver.
 Qed.
 
+Global Instance simpl_and_is_value t `{!IsValue t} :
+  SimplAnd (IsValue t) (λ T, T).
+Proof. split; naive_solver. Qed.
+
+Global Instance simpl_and_has_sort t `{!HasSort t σ} :
+  SimplAnd (HasSort t σ) (λ T, T).
+Proof. split; naive_solver. Qed.
+
 (* sem eq *)
 
 Global Instance simpl_sem_eq_sum_elim_refl N {A B} (x p : A + B) `{!IsProtected p} tA tB :