Prove cubic-finned meithecatte#3

Also modify existing proofs to avoid using a single variable in
two exponents. Their being necessary was an artifact of a shortcoming
of a previous version of the `finned` tactic – and in the current proof,
it is necessary to avoid them instead. Modify all the other proofs for
consistency.

Author: meithecatte

verify/Finned.v

@@ -1,8 +1,18 @@
 From BusyCoq Require Import Individual52.
-From Coq Require Import Lia.
+From Coq Require Import Lia PeanoNat.
+
+Ltac deduce_eq0 :=
+  lazymatch goal with
+  | H: _ + _ = O |- _ =>
+    apply Nat.eq_add_0 in H; destruct H
+  | H: S _ * _ = O |- _ =>
+    apply Nat.eq_mul_0_r in H; [| discriminate]
+  | H: ?x = O |- _ =>
+    is_var x; subst x
+  end.
 
 Ltac single := eapply progress_intro; [prove_step | simpl_tape].
-Ltac goto x := match type of x with
+Ltac goto x := lazymatch type of x with
   | I => exists x
   | _ -> I => exists (x ltac:(lia))
   end; single; finish.
@@ -95,7 +105,7 @@ Ltac maybe_casesplit_at xs :=
   lazymatch xs with
   | _^^?n *> _ =>
     let n' := fresh n "'" in
-    destruct n as [| n']; try lia
+    destruct n as [| n']; try lia; repeat deduce_eq0
   | _ => idtac
   end.
 

verify/Finned3.v

@@ -0,0 +1,65 @@
+(** * Cubic-finned machine #3 (https://bbchallenge.org/10756090) *)
+
+From BusyCoq Require Import Individual52 Finned.
+Set Default Goal Selector "!".
+
+(* NOTE: this swaps L and R compared to the TNF form *)
+Definition tm : TM := fun '(q, s) =>
+  match q, s with
+  | A, 0 => Some (1, L, B)  | A, 1 => Some (1, L, E)
+  | B, 0 => Some (1, R, C)  | B, 1 => Some (1, L, B)
+  | C, 0 => Some (0, L, A)  | C, 1 => Some (0, R, D)
+  | D, 0 => Some (1, R, B)  | D, 1 => Some (1, R, D)
+  | E, 0 => None            | E, 1 => Some (0, L, A)
+  end.
+
+Notation "c --> c'" := (c -[ tm ]-> c')   (at level 40).
+Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
+Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
+
+Close Scope sym.
+
+Inductive I : Type :=
+  | I0 (a b : nat)     (H : 2*a = b + 1) : I
+  | I1 (a b : nat)     (H : 2*a = b) : I
+  | I2 (a b d : nat)   (H : 2*a = b + 2*d + 1) : I
+  | I3 (a b d : nat)   (H : 2*a = b + 2*d + 2) : I
+  | I4 (a d : nat)     (H : a = d) : I
+  | I5 (a b c d : nat) (H : 2*a + d = b + c) : I
+  | I6 (a c d : nat)   (H : 2*a + d = c) : I
+  | I7 (a c d : nat)   (H : 2*a + d = c) : I
+  | I8 (a b c d : nat) (H : 2*a + d = b + c + 3) : I
+  | I9 (a b d : nat)   (H : 2*a + d = b + 2) : I
+  .
+
+Open Scope sym.
+
+Definition f (i : I) : Q * tape :=
+  match i with
+  | I0 a b _ => B;;
+    const 0 <* [1]^^a << 0 <* [1]^^b {{0}} const 0
+  | I1 a b _ => C;;
+    const 0 <* [1]^^a << 0 <* [1]^^b {{0}} const 0
+  | I2 a b d _ => A;;
+    const 0 <* [1]^^a << 0 <* [1]^^b {{1}} [0; 1]^^d *> const 0
+  | I3 a b d _ => E;;
+    const 0 <* [1]^^a << 0 <* [1]^^b {{1}} 1 >> [0; 1]^^d *> const 0
+  | I4 a d _ => A;;
+    const 0 <* [1]^^a {{0}} [0; 1]^^d *> const 0
+  | I5 a b c d _ => B;;
+    const 0 <* [1]^^a << 0 <* [1]^^b {{1}} [1]^^c *> [0; 1]^^d *> const 0
+  | I6 a c d _ => B;;
+    const 0 <* [1]^^a {{0}} 1 >> [1]^^c *> [0; 1]^^d *> const 0
+  | I7 a c d _ => C;;
+    const 0 <* [1]^^a << 1 {{1}} [1]^^c *> [0; 1]^^d *> const 0
+  | I8 a b c d _ => D;;
+    const 0 <* [1]^^a << 0 <* [1]^^b {{1}} [1]^^c *> [0; 1]^^d *> const 0
+  | I9 a b d _ => D;;
+    const 0 <* [1]^^a << 0 <* [1]^^b {{0}} [1; 0]^^d *> const 0
+  end.
+
+Theorem nonhalt : ~ halts tm c0.
+Proof.
+  apply progress_nonhalt_simple with (C := f) (i0 := I4 0 0 eq_refl).
+  intros []; finned.
+Qed.

verify/Finned4.v

@@ -19,16 +19,16 @@ Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
 Close Scope sym.
 
 Inductive I : Type :=
-  | I0 (a b : nat) (H : 2*a = b) : I                 (* 1RB -> I1 *)
-  | I1 (a b : nat) (H : 2*a + 1 = b) : I             (* 0LC -> I2 *)
-  | I2 (a b d : nat) (H : 2*a = b + 2*d) : I         (* 1LD -> I3, I4 *)
-  | I3 (a b d : nat) (H : 2*a = b + 2*d + 1) : I     (* 0LC -> I2 *)
-  | I4 (a : nat) : I                                 (* 1RA -> I0, I5 *)
-  | I5 (a b c d : nat) (H : 2*a + d + 1 = b + c) : I (* 1LA -> I5, I6 *)
-  | I6 (a c d : nat) (H : 2*a + d + 1 = c) : I       (* 1RB -> I7 *)
-  | I7 (a c d : nat) (H : 2*a + d + 1 = c) : I       (* 0RE -> I8 *)
-  | I8 (a b c d : nat) (H : 2*a + d = b + c + 2) : I (* 1RE -> I8, I9 *)
-  | I9 (a b d : nat) (H : 2*a + d = b + 1) : I       (* 1RA -> I5 *)
+  | I0 (a b : nat)     (H : 2*a = b) : I
+  | I1 (a b : nat)     (H : 2*a + 1 = b) : I
+  | I2 (a b d : nat)   (H : 2*a = b + 2*d) : I
+  | I3 (a b d : nat)   (H : 2*a = b + 2*d + 1) : I
+  | I4 (a d : nat)     (H : a = d) : I
+  | I5 (a b c d : nat) (H : 2*a + d + 1 = b + c) : I
+  | I6 (a c d : nat)   (H : 2*a + d + 1 = c) : I
+  | I7 (a c d : nat)   (H : 2*a + d + 1 = c) : I
+  | I8 (a b c d : nat) (H : 2*a + d = b + c + 2) : I
+  | I9 (a b d : nat)   (H : 2*a + d = b + 1) : I
   .
 
 Open Scope sym.
@@ -43,8 +43,8 @@ Definition f (i : I) : Q * tape :=
     const 0 <* [1]^^a << 0 <* [1]^^b {{1}} [0; 1]^^d *> const 0
   | I3 a b d _ => D;;
     const 0 <* [1]^^a << 0 <* [1]^^b {{1}} 1 >> [0; 1]^^d *> const 0
-  | I4 a => D;;
-    const 0 <* [1]^^a {{0}} 1 >> [0; 1]^^a *> const 0
+  | I4 a d _ => D;;
+    const 0 <* [1]^^a {{0}} 1 >> [0; 1]^^d *> const 0
   | I5 a b c d _ => A;;
     const 0 <* [1]^^a << 0 <* [1]^^b {{1}} [1]^^c *> [0; 1]^^d *> const 0
   | I6 a c d _ => A;;

verify/Finned5.v

@@ -19,16 +19,16 @@ Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
 Close Scope sym.
 
 Inductive I : Type :=
-  | I0 (a b : nat) (H : 2*a = b) : I                 (* 1RB -> I1 *)
-  | I1 (a b : nat) (H : 2*a + 1 = b) : I             (* 0LC -> I2 *)
-  | I2 (a b d : nat) (H : 2*a = b + 2*d) : I         (* 1LD -> I3, I4 *)
-  | I3 (a b d : nat) (H : 2*a = b + 2*d + 1) : I     (* 0LC -> I2 *)
-  | I4 (a : nat) : I                                 (* 1LA -> I5, I6 *)
-  | I5 (a b c d : nat) (H : 2*a + d + 1 = b + c) : I (* 1LA -> I5, I6 *)
-  | I6 (a c d : nat) (H : 2*a + d + 1 = c) : I       (* 1RB -> I7 *)
-  | I7 (a c d : nat) (H : 2*a + d + 1 = c) : I       (* 0RE -> I8 *)
-  | I8 (a b c d : nat) (H : 2*a + d = b + c + 2) : I (* 1RE -> I8, I9 *)
-  | I9 (a b d : nat) (H : 2*a + d = b + 1) : I       (* 1RA -> I0, I5 *)
+  | I0 (a b : nat)     (H : 2*a = b) : I
+  | I1 (a b : nat)     (H : 2*a + 1 = b) : I
+  | I2 (a b d : nat)   (H : 2*a = b + 2*d) : I
+  | I3 (a b d : nat)   (H : 2*a = b + 2*d + 1) : I
+  | I4 (a d : nat)     (H : a = d) : I
+  | I5 (a b c d : nat) (H : 2*a + d + 1 = b + c) : I
+  | I6 (a c d : nat)   (H : 2*a + d + 1 = c) : I
+  | I7 (a c d : nat)   (H : 2*a + d + 1 = c) : I
+  | I8 (a b c d : nat) (H : 2*a + d = b + c + 2) : I
+  | I9 (a b d : nat)   (H : 2*a + d = b + 1) : I
   .
 
 Open Scope sym.
@@ -43,8 +43,8 @@ Definition f (i : I) : Q * tape :=
     const 0 <* [1]^^a << 0 <* [1]^^b {{1}} [0; 1]^^d *> const 0
   | I3 a b d _ => D;;
     const 0 <* [1]^^a << 0 <* [1]^^b {{1}} 1 >> [0; 1]^^d *> const 0
-  | I4 a => D;;
-    const 0 <* [1]^^a {{0}} 1 >> [0; 1]^^a *> const 0
+  | I4 a d _ => D;;
+    const 0 <* [1]^^a {{0}} 1 >> [0; 1]^^d *> const 0
   | I5 a b c d _ => A;;
     const 0 <* [1]^^a << 0 <* [1]^^b {{1}} [1]^^c *> [0; 1]^^d *> const 0
   | I6 a c d _ => A;;

verify/Makefile

@@ -3,7 +3,7 @@ COQMFFLAGS := -Q . BusyCoq
 ALLVFILES := LibTactics.v Helper.v Pigeonhole.v TM.v Compute.v Flip.v Permute.v DirectedCompute.v Subtape.v \
 	Cyclers.v TranslatedCyclers.v BackwardsReasoning.v Bouncers.v Individual.v \
 	BB52.v Individual52.v FixedBin.v ShiftOverflow.v ShiftOverflowBins.v Skelet15.v Skelet26.v Skelet33.v Skelet34.v Skelet35.v \
-	Skelet10.v Skelet17.v Skelet1.v Finned.v Finned1.v Finned2.v Finned4.v Finned5.v Extraction.v \
+	Skelet10.v Skelet17.v Skelet1.v Finned.v Finned1.v Finned2.v Finned3.v Finned4.v Finned5.v Extraction.v \
 	BB33.v Individual33.v
 
 all: check verify skelet1