proof(coq): tighten sumbool tactic patterns in file_operations + symlink_operations

Fix `destruct (list_eq_dec p p)` → exhaustive named branches in 3 files.
Fixes the same issue as 1ef841c but in file_operations.v and symlink_operations.v.
Also tightens create_file_has_parent and mkdir_creates_empty_dir argument handling.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

proofs/coq/file_operations.v

@@ -77,7 +77,9 @@ Theorem delete_file_removes_path :
 Proof.
   intros p fs Hpre [node Hexists].
   unfold delete_file, fs_update in Hexists.
-  destruct (list_eq_dec String.string_dec p p); discriminate.
+  destruct (list_eq_dec String.string_dec p p) as [_ | Hneq].
+  - discriminate.
+  - exact (Hneq eq_refl).
 Qed.
 
 (** * File Reversibility Theorem *)
@@ -95,10 +97,12 @@ Proof.
   destruct (list_eq_dec String.string_dec p p').
   - (* p = p' *)
     subst.
-    destruct (list_eq_dec String.string_dec p' p'); [|contradiction].
-    destruct Hpre as [Hnotexists _].
-    destruct Hnotexists.
-    assumption.
+    destruct (list_eq_dec String.string_dec p' p') as [_ | Hneq].
+    + destruct Hpre as [Hnotexists _].
+      destruct (fs p') as [node |] eqn:Hfsp.
+      * exfalso. apply Hnotexists. unfold path_exists. exists node. exact Hfsp.
+      * reflexivity.
+    + exact (Hneq eq_refl).
   - (* p <> p' *)
     destruct (list_eq_dec String.string_dec p p'); [contradiction|].
     reflexivity.
@@ -136,12 +140,9 @@ Proof.
   destruct Hparent as [node Hnode].
   exists node.
   unfold create_file, fs_update.
-  destruct (list_eq_dec String.string_dec p (parent_path p)).
-  - (* p = parent_path p would mean path_exists p fs (from parentExists),
-       contradicting notExists. Derive contradiction. *)
-    subst. exfalso.
-    apply HnotExists.
-    exists node. assumption.
+  destruct (list_eq_dec String.string_dec p (parent_path p)) as [Heq | _].
+  - (* p = parent_path p — contradicts HnotExists: p already exists via Hnode *)
+    exfalso. apply HnotExists. exists node. rewrite Heq. exact Hnode.
   - assumption.
 Qed.
 

proofs/coq/filesystem_composition.v

@@ -470,18 +470,16 @@ Proof.
     exists node.
     split; [| assumption].
     unfold mkdir, fs_update.
-    destruct (list_eq_dec String.string_dec p (parent_path p)).
-    + (* p = parent_path p would mean path_exists p fs via parentExists,
-         contradicting notExists *)
-      subst. exfalso.
-      apply Hnotexists.
-      exists node. assumption.
+    destruct (list_eq_dec String.string_dec p (parent_path p)) as [Heq | _].
+    + (* p = parent_path p — contradicts Hnotexists: p already exists via Hnode *)
+      exfalso. apply Hnotexists. exists node. rewrite Heq. exact Hnode.
     + assumption.
   - (* p <> root_path *)
     intro Hroot.
     subst.
-    destruct Hnotexists.
-    apply path_exists_empty_fs_root.
+    apply Hnotexists.
+    unfold parent_exists in Hparent. simpl in Hparent.
+    exact Hparent.
 Qed.
 
 (** mkdir preserves well-formedness: adding a node whose parent exists

proofs/coq/symlink_operations.v

@@ -48,7 +48,9 @@ Theorem unlink_removes_path :
 Proof.
   intros p fs Hexists [node Hnode].
   unfold unlink, fs_update in Hnode.
-  destruct (list_eq_dec String.string_dec p p); discriminate.
+  destruct (list_eq_dec String.string_dec p p) as [_ | Hneq].
+  - discriminate.
+  - exact (Hneq eq_refl).
 Qed.
 
 (** * Reversibility Theorem *)