sui: more proofs for the stack

formal-land · Dec 17, 2024 · 9fa945a · 9fa945a
1 parent 3607080
commit 9fa945a
Show file tree

Hide file tree

Showing 6 changed files with 402 additions and 187 deletions.
diff --git a/CoqOfRust/RecordUpdate.v b/CoqOfRust/RecordUpdate.v
@@ -72,6 +72,8 @@ Class Setter{R E: Type}(getter: R -> E): Type :=
   set : E -> R -> R.
 
 Arguments set {R E} (getter) {Setter} (fieldUpdater) (r).
+(* Reduce when calling the [cbn] tactic *)
+Arguments set /.
 
 Global Hint Extern 1 (@Setter ?R ?E ?getter) =>
   exact_setter R getter : typeclass_instances.

diff --git a/CoqOfRust/core/simulations/eq.v b/CoqOfRust/core/simulations/eq.v
@@ -2,6 +2,14 @@ Module Eq.
   Class Trait (Self : Set) : Set := {
     eqb: Self -> Self -> bool
   }.
+
+  Module Valid.
+  (** An equality [equal] is valid when it decides the standard equality [=]. *)
+  Definition t {Self : Set} `{Trait Self} (domain : Self -> Prop) : Prop :=
+    forall x y,
+    domain x -> domain y ->
+    (x = y) <-> (eqb x y = true).
+  End Valid.
 End Eq.
 
 Module Notations.