proof(coq): replace 5 decidability axioms with constructive proofs

hyperpolymath · claude · hyperpolymath · commit 794c56856406 · 2026-04-12T12:08:13.000+01:00
posix_errors.v had two structural bugs: 1. Decision procedures declared as Axiom AFTER safe_* definitions that used them (forward-reference error in Coq's sequential processing). 2. safe_* definitions used `negb (sumbool_val)` which is a type error — negb : bool -> bool, but the sumbool {P} + {~P} is not a bool. Fix: - Moved decision procedures to BEFORE safe_* definitions. - Proved path_exists_dec, is_directory_dec, is_file_dec, has_write_permission_dec, path_eq_dec constructively by case-splitting on the Filesystem function (Path -> option FSNode) and the FSNode fields. - Kept is_empty_dir_dec as Axiom with full justification: universal quantification over an infinite-domain function cannot be decided constructively; finite-map refactor removes this axiom. - Restructured safe_* definitions to use nested `if` on sumbool (correct) instead of `negb (sumbool_val)` (type error). All existing theorems and proofs preserved with minimal changes. filesystem_composition.v: added detailed proof-strategy comments to well_formed_ancestor_exists and mkdir_preserves_well_formed axioms, referencing PROOF_HOLES_AUDIT.md items #1 and #2. functional_extensionality: already correctly imported in filesystem_model.v; all other files get it transitively via Require Import filesystem_model. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
diff --git a/proofs/coq/filesystem_composition.v b/proofs/coq/filesystem_composition.v
@@ -298,8 +298,17 @@ Definition well_formed (fs : Filesystem) : Prop :=
     path_exists (parent_path p) fs.
 
 (** Well-formedness transitive closure: if a strict descendant exists,
-    all ancestors down to the prefix exist. Provable by induction on
-    path length difference, using well_formed at each step. *)
+    all ancestors down to the prefix exist.
+
+    Proof strategy (deferred): induction on (length child - length p).
+    Base: length diff = 0 → child = p, contradicts child ≠ p.
+    Step: well_formed gives path_exists (parent_path child) fs; parent_path
+    child has length (length child - 1); path_prefix p (parent_path child) holds
+    (since p is still a proper prefix); recurse.
+
+    Deferred because it requires a path-length lemma and a path_prefix/parent_path
+    interaction lemma, both straightforward but adding ~30 lines of scaffolding.
+    Tracked as proof debt item #1 in docs/PROOF_HOLES_AUDIT.md. *)
 Axiom well_formed_ancestor_exists :
   forall fs p child,
     well_formed fs ->
@@ -373,7 +382,19 @@ Proof.
 Qed.
 
 (** mkdir preserves well-formedness: adding a node whose parent exists
-    maintains the parent-existence invariant for all paths. *)
+    maintains the parent-existence invariant for all paths.
+
+    Proof strategy (deferred): unfold well_formed; for any q ≠ root_path, split
+    on whether q = p (just added by mkdir). If q = p: parent_path p exists by
+    mkdir_precondition (parent_exists clause). If q ≠ p: fs_update preserves
+    the original fs everywhere except p, so path_exists q (mkdir p fs) implies
+    path_exists q fs (since q ≠ p), and then well_formed fs gives
+    path_exists (parent_path q) fs; finally parent_path q ≠ p (because mkdir
+    only adds a fresh path with no children yet), so
+    path_exists (parent_path q) (mkdir p fs) follows.
+
+    Deferred: the "parent_path q ≠ p" sub-goal requires a lemma about
+    path_prefix ordering. Tracked as proof debt item #2 in PROOF_HOLES_AUDIT.md. *)
 Axiom mkdir_preserves_well_formed :
   forall p fs,
     well_formed fs ->
diff --git a/proofs/coq/posix_errors.v b/proofs/coq/posix_errors.v
@@ -4,6 +4,12 @@
     Proves error handling correctness and error-free operation equivalence.
 
     This extends the pure functional model to handle real-world error cases.
+
+    Proof status:
+    - 5 of 6 decision procedures proved constructively (from Filesystem semantics).
+    - is_empty_dir_dec remains axiomatic: requires Classical or finite-map refactor.
+    - safe_* definitions use nested `if` on sumbool (not negb, which requires bool).
+    - functional_extensionality from filesystem_model transitive import.
 *)
 
 Require Import String.
@@ -38,68 +44,142 @@ Inductive OperationResult (A : Type) : Type :=
 Arguments Success {A}.
 Arguments Error {A}.
 
-(** * Safe Operations with Error Handling *)
+(** * Decision Procedures
+
+    Must appear before the safe_* definitions that use them.
+
+    Four decision procedures are proved constructively by inspecting the
+    Filesystem function (Path -> option FSNode) directly.
+    path_eq_dec follows from list_eq_dec + String.string_dec.
+    is_empty_dir_dec is axiomatic — see justification below. *)
+
+(** path_exists is decidable by case analysis on (fs p). *)
+Lemma path_exists_dec : forall p fs, {path_exists p fs} + {~ path_exists p fs}.
+Proof.
+  intros p fs.
+  unfold path_exists.
+  destruct (fs p) as [node|].
+  - left. exists node. reflexivity.
+  - right. intros [node H]. discriminate.
+Defined.
+
+(** is_directory is decidable by inspecting the node_type field. *)
+Lemma is_directory_dec : forall p fs, {is_directory p fs} + {~ is_directory p fs}.
+Proof.
+  intros p fs.
+  unfold is_directory.
+  destruct (fs p) as [[ntype perms]|].
+  - destruct ntype.
+    + (* File *) right. intros [perms' H]. inversion H.
+    + (* Directory *) left. exists perms. reflexivity.
+  - right. intros [perms H]. discriminate.
+Defined.
+
+(** is_file is decidable by inspecting the node_type field. *)
+Lemma is_file_dec : forall p fs, {is_file p fs} + {~ is_file p fs}.
+Proof.
+  intros p fs.
+  unfold is_file.
+  destruct (fs p) as [[ntype perms]|].
+  - destruct ntype.
+    + (* File *) left. exists perms. reflexivity.
+    + (* Directory *) right. intros [perms' H]. inversion H.
+  - right. intros [perms H]. discriminate.
+Defined.
+
+(** has_write_permission is decidable by inspecting the node and its writable flag. *)
+Lemma has_write_permission_dec : forall p fs, {has_write_permission p fs} + {~ has_write_permission p fs}.
+Proof.
+  intros p fs.
+  unfold has_write_permission.
+  destruct (fs p) as [node|].
+  - destruct (writable (permissions node)) eqn:Hw.
+    + left. exists node. split; [reflexivity | assumption].
+    + right. intros [node' [Heq Hwr]].
+      inversion Heq. subst. rewrite Hw in Hwr. discriminate.
+  - right. intros [node [H _]]. discriminate.
+Defined.
+
+(** Path equality is decidable: Path = list string, decided by list_eq_dec + string_dec. *)
+Lemma path_eq_dec : forall p1 p2 : Path, {p1 = p2} + {p1 <> p2}.
+Proof.
+  apply list_eq_dec.
+  apply String.string_dec.
+Defined.
+
+(** is_empty_dir is NOT decidable constructively with the current model.
+
+    is_empty_dir p fs requires:
+      forall child : Path, path_prefix p child -> child <> p -> ~ path_exists child fs.
+
+    With Filesystem = Path -> option FSNode (a function over an infinite domain),
+    there is no finite enumeration of all Path values, so this universal
+    quantification cannot be discharged constructively.
+
+    Justification: in the operational model, every reachable filesystem is
+    produced by a finite sequence of mkdir / rmdir / create_file / delete_file
+    operations, so the set of inhabited paths is always finite in practice.
+    Constructive decidability requires changing the Filesystem representation
+    to a finite map (e.g., list (Path * FSNode) or MSetAVL), at which point
+    is_empty_dir can be decided by scanning the entries.
+
+    Migration path: switch Filesystem to FMaps.t FSNode and reprove. *)
+Axiom is_empty_dir_dec : forall p fs, {is_empty_dir p fs} + {~ is_empty_dir p fs}.
+
+(** * Safe Operations with Error Handling
+
+    safe_* definitions use nested `if` on sumbool values.
+    Using `negb (sumbool_val)` is a type error (negb : bool -> bool, not sumbool)
+    so we invert the condition by nesting the positive branch first. *)
 
 (** Safe mkdir - returns error codes instead of requiring preconditions *)
 Definition safe_mkdir (p : Path) (fs : Filesystem) : OperationResult Filesystem :=
   if path_exists_dec p fs then
-    Error EEXIST
-  else if negb (path_exists_dec (parent_path p) fs) then
-    Error ENOENT
-  else if negb (is_directory_dec (parent_path p) fs) then
-    Error ENOTDIR
-  else if negb (has_write_permission_dec (parent_path p) fs) then
-    Error EACCES
-  else
-    Success (mkdir p fs).
+    Error EEXIST                                     (* p already exists *)
+  else if path_exists_dec (parent_path p) fs then
+    if is_directory_dec (parent_path p) fs then
+      if has_write_permission_dec (parent_path p) fs then
+        Success (mkdir p fs)
+      else Error EACCES
+    else Error ENOTDIR
+  else Error ENOENT.                                 (* parent not found *)
 
 (** Safe rmdir - returns error codes *)
 Definition safe_rmdir (p : Path) (fs : Filesystem) : OperationResult Filesystem :=
-  if negb (path_exists_dec p fs) then
-    Error ENOENT
-  else if negb (is_directory_dec p fs) then
-    Error ENOTDIR
-  else if negb (is_empty_dir_dec p fs) then
-    Error ENOTEMPTY
-  else if negb (has_write_permission_dec (parent_path p) fs) then
-    Error EACCES
-  else if path_eq_dec p root_path then
-    Error EACCES  (* Cannot remove root *)
-  else
-    Success (rmdir p fs).
+  if path_exists_dec p fs then
+    if is_directory_dec p fs then
+      if is_empty_dir_dec p fs then
+        if has_write_permission_dec (parent_path p) fs then
+          if path_eq_dec p root_path then
+            Error EACCES                             (* cannot remove root *)
+          else
+            Success (rmdir p fs)
+        else Error EACCES
+      else Error ENOTEMPTY
+    else Error ENOTDIR
+  else Error ENOENT.
 
 (** Safe create_file - returns error codes *)
 Definition safe_create_file (p : Path) (fs : Filesystem) : OperationResult Filesystem :=
   if path_exists_dec p fs then
     Error EEXIST
-  else if negb (path_exists_dec (parent_path p) fs) then
-    Error ENOENT
-  else if negb (is_directory_dec (parent_path p) fs) then
-    Error ENOTDIR
-  else if negb (has_write_permission_dec (parent_path p) fs) then
-    Error EACCES
-  else
-    Success (create_file p fs).
+  else if path_exists_dec (parent_path p) fs then
+    if is_directory_dec (parent_path p) fs then
+      if has_write_permission_dec (parent_path p) fs then
+        Success (create_file p fs)
+      else Error EACCES
+    else Error ENOTDIR
+  else Error ENOENT.
 
 (** Safe delete_file - returns error codes *)
 Definition safe_delete_file (p : Path) (fs : Filesystem) : OperationResult Filesystem :=
-  if negb (path_exists_dec p fs) then
-    Error ENOENT
-  else if negb (is_file_dec p fs) then
-    Error EISDIR
-  else if negb (has_write_permission_dec (parent_path p) fs) then
-    Error EACCES
-  else
-    Success (delete_file p fs).
-
-(** * Decision Procedures (axiomatized for now) *)
-
-Axiom path_exists_dec : forall p fs, {path_exists p fs} + {~ path_exists p fs}.
-Axiom is_directory_dec : forall p fs, {is_directory p fs} + {~ is_directory p fs}.
-Axiom is_file_dec : forall p fs, {is_file p fs} + {~ is_file p fs}.
-Axiom has_write_permission_dec : forall p fs, {has_write_permission p fs} + {~ has_write_permission p fs}.
-Axiom is_empty_dir_dec : forall p fs, {is_empty_dir p fs} + {~ is_empty_dir p fs}.
-Axiom path_eq_dec : forall p1 p2 : Path, {p1 = p2} + {p1 <> p2}.
+  if path_exists_dec p fs then
+    if is_file_dec p fs then
+      if has_write_permission_dec (parent_path p) fs then
+        Success (delete_file p fs)
+      else Error EACCES
+    else Error EISDIR
+  else Error ENOENT.
 
 (** * Error Handling Correctness Theorems *)
 
@@ -113,7 +193,6 @@ Proof.
   - (* -> *)
     unfold safe_mkdir.
     intros H.
-    (* Check each condition *)
     destruct (path_exists_dec p fs); [discriminate|].
     destruct (path_exists_dec (parent_path p) fs); [|discriminate].
     destruct (is_directory_dec (parent_path p) fs); [|discriminate].
@@ -193,7 +272,6 @@ Proof.
   intros p fs Hnoexist Hnoparent.
   unfold safe_mkdir.
   destruct (path_exists_dec p fs); [contradiction|].
-  simpl.
   unfold parent_exists in Hnoparent.
   destruct (path_exists_dec (parent_path p) fs); [contradiction|].
   reflexivity.
@@ -219,7 +297,6 @@ Proof.
   intros p fs Hexists Hnotdir.
   unfold safe_rmdir.
   destruct (path_exists_dec p fs); [|contradiction].
-  simpl.
   destruct (is_directory_dec p fs); [contradiction|].
   reflexivity.
 Qed.
@@ -233,9 +310,7 @@ Proof.
   intros p fs Hisdir Hnotempty.
   unfold safe_rmdir.
   destruct (path_exists_dec p fs).
-  - simpl.
-    destruct (is_directory_dec p fs); [|contradiction].
-    simpl.
+  - destruct (is_directory_dec p fs); [|contradiction].
     destruct (is_empty_dir_dec p fs); [contradiction|].
     reflexivity.
   - exfalso.
@@ -276,6 +351,8 @@ Qed.
     ✓ Correctness: Success iff preconditions hold
     ✓ Error code correctness: Each error matches specific violation
     ✓ Reversibility preserved under error handling
+    ✓ 5/6 decision procedures proved constructively (Lemma, not Axiom)
+    ✗ is_empty_dir_dec: justified axiom, requires finite-map Filesystem for proof
 
     This enables:
     - Realistic implementation with proper error reporting
