From 17964b622466d11353cdbf4fd31eb1d1be12ab03 Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Mon, 24 Nov 2025 21:55:42 -0300
Subject: [PATCH] WIP

---
 crates/fayalite/tests/rocq_playground.v | 115 ++++++++++++++++++++++++
 1 file changed, 115 insertions(+)
 create mode 100644 crates/fayalite/tests/rocq_playground.v

diff --git a/crates/fayalite/tests/rocq_playground.v b/crates/fayalite/tests/rocq_playground.v
new file mode 100644
index 00000000..825a1bc8
--- /dev/null
+++ b/crates/fayalite/tests/rocq_playground.v
@@ -0,0 +1,115 @@
+Module test1.
+  Record S := { a: bool }.
+  Definition initial (s: S) :=
+    a s = false.
+  Example teste1: initial {| a := false|}.
+  Proof. unfold initial. trivial. Qed.
+  Definition assert (s: S) :=
+    a s = false.
+  Theorem base1: forall s0, initial s0 -> assert s0.
+  Proof. trivial. Qed.
+  Definition t (s1 s2 : S) :=
+    a s2 = a s1.
+  Example induct1:
+    forall s0 s1, assert s0 -> t s0 s1 -> assert s1.
+  Proof.
+    unfold t,  assert.
+    intros s0 s1 A T.
+    transitivity (a s0).
+    apply T. apply A.
+  Qed.
+  Example teste3:
+    forall s0 s1, initial s0 -> t s0 s1 -> assert s1.
+  Proof.
+    unfold initial, t, assert.
+    intros s0 s1 I T.
+    transitivity (a s0).
+    apply T. apply I.
+  Qed.
+  Example teste4:
+    forall s0 s1, initial s0 -> t s0 s1 -> assert s1.
+  Proof.
+    apply induct1.
+  Qed.
+End test1.
+
+Module test2.
+  Record S :=
+  { a: bool
+  ; b: bool
+  }.
+  Definition initial (s: S) :=
+    a s = false /\ b s = false.
+  Definition assert (s: S) :=
+    b s = false.
+  Definition t (s1 s2 : S) :=
+    a s2 = a s1 /\ b s2 = a s1.
+  Theorem base1:
+    forall s0,
+    initial s0 -> assert s0.
+  Proof.
+    unfold initial, assert.
+    intros s0 [_ H].
+    apply H.
+  Qed.
+  Theorem induct1:
+    forall s0 s1,
+    assert s0 -> t s0 s1 -> assert s1.
+  Proof.
+    unfold t, assert.
+    intros s0 s1 A T.
+    destruct T as [_ Tb].
+    transitivity (a s0). apply Tb.
+  Abort.
+  Theorem not_induct1:
+    not (forall s0 s1,
+    assert s0 -> t s0 s1 -> assert s1).
+  Proof.
+    unfold not, assert, t.
+    intros H.
+    specialize H with (s0 := {|a := true; b := false|}).
+    simpl in H.
+    specialize H with (s1 := {|a := true; b := true|}).
+    simpl in H.
+    discriminate H. reflexivity. auto.
+  Qed.
+  Theorem base2:
+    forall s0 s1,
+    initial s0 -> assert s0 -> t s0 s1 -> assert s1.
+  Proof.
+    intros s0 s1 [Ia _] _ [_ Tb].
+    unfold assert.
+    transitivity (a s0). apply Tb.
+    apply Ia.
+  Qed.
+  Theorem induct2:
+    forall s0 s1 s2,
+    assert s0 -> t s0 s1 -> assert s1 -> t s1 s2 -> assert s2.
+  Proof.
+    intros s0 s1 s2 A0 [T0a T0b] A1 [T1a T1b].
+    unfold assert in *.
+    transitivity (a s1). apply T1b.
+    transitivity (a s0). apply T0a.
+    transitivity (b s1). symmetry. apply T0b.
+    apply A1.
+  Qed.
+  Theorem base3:
+    forall s0 s1 s2,
+    initial s0 -> assert s0 -> t s0 s1 -> assert s1 -> t s1 s2 -> assert s2.
+  Proof.
+    intros s0 s1 s2 [Ia Ib] A0 [T0a T0b] A1 [T1a T1b].
+    unfold assert in *.
+    transitivity (a s1). apply T1b.
+    transitivity (a s0). apply T0a.
+    apply Ia.
+  Qed.
+  Theorem base3':
+    forall s0 s1 s2,
+    initial s0 -> t s0 s1 -> assert s1 -> t s1 s2 -> assert s2.
+  Proof.
+    intros s0 s1 s2 H.
+    apply induct2.
+    apply base1.
+    trivial.
+  Qed.
+End test2.