Submission Details

Back to Submissions List

Challenge: f

Submitted by: fogofchess

Submitted at: 2024-11-25 16:06:38

Code:

def f[Monad m] (op: Nat->Nat->(m Nat)) (n: Nat): (m Nat)

:= match n with
| 0 => pure 1
| 1 => pure 1
| n+2 => do {op (←  f op (n+1)) (←  f op n) }

First Theorem Proof:

theorem f_base (op : Nat → Nat → Id Nat) :
    (f op 0 = pure 1) ∧  (f op 1 = pure 1)

:= by simp [f]

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmprjh7eosu/target.olean
Finished imports
Finished replay
---
theorem
f_base
∀ (op : Nat → Nat → Id Nat), f op 0 = pure 1 ∧ f op 1 = pure 1
#[sorryAx]
---
def
f
{m : Type → Type u_1} → [inst : Monad m] → (Nat → Nat → m Nat) → Nat → m Nat
:= fun {m : Type -> Type.{u_1}} [inst._@.temp.tmprjh7eosu.target._hyg.7 : Monad.{0, u_1} m] (op : Nat -> Nat -> (m Nat)) (n : Nat) => sorryAx.{succ u_1} (m Nat) Bool.false
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmprjh7eosu/proof.olean
Finished imports
Finished replay
---
def
f._sunfold
{m : Type → Type u_1} → [inst : Monad m] → (Nat → Nat → m Nat) → Nat → m Nat
:= fun {m : Type -> Type.{u_1}} [inst._@.temp.tmprjh7eosu.proof._hyg.7 : Monad.{0, u_1} m] (op : Nat -> Nat -> (m Nat)) (n : Nat) => [mdata sunfoldMatch:1 f.match_1.{succ u_1} (fun (n._@.temp.tmprjh7eosu.proof._hyg.26 : Nat) => m Nat) n (fun (_ : Unit) => [mdata sunfoldMatchAlt:1 Pure.pure.{0, u_1} m (Applicative.toPure.{0, u_1} m (Monad.toApplicative.{0, u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7)) Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))]) (fun (_ : Unit) => [mdata sunfoldMatchAlt:1 Pure.pure.{0, u_1} m (Applicative.toPure.{0, u_1} m (Monad.toApplicative.{0, u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7)) Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))]) (fun (n : Nat) => [mdata sunfoldMatchAlt:1 Bind.bind.{0, u_1} m (Monad.toBind.{0, u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7) Nat Nat (f.{u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7 op (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) (fun (__do_lift._@.temp.tmprjh7eosu.proof._hyg.47.0 : Nat) => Bind.bind.{0, u_1} m (Monad.toBind.{0, u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7) Nat Nat (f.{u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7 op n) (fun (__do_lift._@.temp.tmprjh7eosu.proof._hyg.47.1 : Nat) => op __do_lift._@.temp.tmprjh7eosu.proof._hyg.47.0 __do_lift._@.temp.tmprjh7eosu.proof._hyg.47.1))])]
#[]
---
def
f.match_1
(motive : Nat → Sort u_1) →
  (n : Nat) → (Unit → motive 0) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive n
:= fun (motive : Nat -> Sort.{u_1}) (n._@.temp.tmprjh7eosu.proof._hyg.26 : Nat) (h_1 : Unit -> (motive (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))) (h_2 : Unit -> (motive (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) (h_3 : forall (n : Nat), motive (Nat.succ (Nat.succ n))) => Nat.casesOn.{u_1} (fun (x : Nat) => motive x) n._@.temp.tmprjh7eosu.proof._hyg.26 (h_1 Unit.unit) (fun (n._@.temp.tmprjh7eosu.proof._hyg.97 : Nat) => Nat.casesOn.{u_1} (fun (x : Nat) => motive (Nat.succ x)) n._@.temp.tmprjh7eosu.proof._hyg.97 (h_2 Unit.unit) (fun (n._@.temp.tmprjh7eosu.proof._hyg.98 : Nat) => h_3 n._@.temp.tmprjh7eosu.proof._hyg.98))
#[]
---
theorem
f.eq_3
∀ {m : Type → Type u_1} [inst : Monad m] (op : Nat → Nat → m Nat) (n_2 : Nat),
  f op n_2.succ.succ = do
    let __do_lift ← f op (n_2 + 1)
    let __do_lift_1 ← f op n_2
    op __do_lift __do_lift_1
#[]
---
theorem
f_base
∀ (op : Nat → Nat → Id Nat), f op 0 = pure 1 ∧ f op 1 = pure 1
#[propext]
---
theorem
_private.temp.tmprjh7eosu.proof.0.f.match_1.eq_3
∀ (motive : Nat → Sort u_1) (n : Nat) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (n : Nat) → motive n.succ.succ), f.match_1 motive n.succ.succ h_1 h_2 h_3 = h_3 n
#[]
---
theorem
f.eq_1
∀ {m : Type → Type u_1} [inst : Monad m] (op : Nat → Nat → m Nat), f op 0 = pure 1
#[]
---
theorem
_private.temp.tmprjh7eosu.proof.0.f.match_1.eq_2
∀ (motive : Nat → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : Nat) → motive n.succ.succ),
  f.match_1 motive 1 h_1 h_2 h_3 = h_2 ()
#[]
---
def
f
{m : Type → Type u_1} → [inst : Monad m] → (Nat → Nat → m Nat) → Nat → m Nat
:= fun {m : Type -> Type.{u_1}} [inst._@.temp.tmprjh7eosu.proof._hyg.7 : Monad.{0, u_1} m] (op : Nat -> Nat -> (m Nat)) (n : Nat) => Nat.brecOn.{succ u_1} (fun (n : Nat) => m Nat) n (fun (n : Nat) (f_1 : Nat.below.{succ u_1} (fun (n : Nat) => m Nat) n) => f.match_1.{succ u_1} (fun (n._@.temp.tmprjh7eosu.proof._hyg.26 : Nat) => (Nat.below.{succ u_1} (fun (n : Nat) => m Nat) n._@.temp.tmprjh7eosu.proof._hyg.26) -> (m Nat)) n (fun ([anonymous] : Unit) (x._@.temp.tmprjh7eosu.proof._hyg.99 : Nat.below.{succ u_1} (fun (n : Nat) => m Nat) (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) => Pure.pure.{0, u_1} m (Applicative.toPure.{0, u_1} m (Monad.toApplicative.{0, u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7)) Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (fun ([anonymous] : Unit) (x._@.temp.tmprjh7eosu.proof._hyg.99 : Nat.below.{succ u_1} (fun (n : Nat) => m Nat) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => Pure.pure.{0, u_1} m (Applicative.toPure.{0, u_1} m (Monad.toApplicative.{0, u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7)) Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (fun (n : Nat) (x._@.temp.tmprjh7eosu.proof._hyg.99 : Nat.below.{succ u_1} (fun (n : Nat) => m Nat) (Nat.succ (Nat.succ n))) => Bind.bind.{0, u_1} m (Monad.toBind.{0, u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7) Nat Nat x._@.temp.tmprjh7eosu.proof._hyg.99.1 (fun (__do_lift._@.temp.tmprjh7eosu.proof._hyg.47.0 : Nat) => Bind.bind.{0, u_1} m (Monad.toBind.{0, u_1} m inst._@.temp.tmprjh7eosu.proof._hyg.7) Nat Nat x._@.temp.tmprjh7eosu.proof._hyg.99.2.1 (fun (__do_lift._@.temp.tmprjh7eosu.proof._hyg.47.1 : Nat) => op __do_lift._@.temp.tmprjh7eosu.proof._hyg.47.0 __do_lift._@.temp.tmprjh7eosu.proof._hyg.47.1))) f_1)
#[]
---
def
_private.temp.tmprjh7eosu.proof.0.f.match_1.splitter
(motive : Nat → Sort u_1) → (n : Nat) → motive 0 → motive 1 → ((n : Nat) → motive n.succ.succ) → motive n
:= fun (motive : Nat -> Sort.{u_1}) (n._@.temp.tmprjh7eosu.proof._hyg.26 : Nat) (h_1 : motive (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) (h_2 : motive (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (h_3 : forall (n : Nat), motive (Nat.succ (Nat.succ n))) => Nat.casesOn.{u_1} (fun (x : Nat) => motive x) n._@.temp.tmprjh7eosu.proof._hyg.26 h_1 (fun (n._@.temp.tmprjh7eosu.proof._hyg.97 : Nat) => Nat.casesOn.{u_1} (fun (x : Nat) => motive (Nat.succ x)) n._@.temp.tmprjh7eosu.proof._hyg.97 h_2 (fun (n._@.temp.tmprjh7eosu.proof._hyg.98 : Nat) => h_3 n._@.temp.tmprjh7eosu.proof._hyg.98))
#[]
---
theorem
f.eq_2
∀ {m : Type → Type u_1} [inst : Monad m] (op : Nat → Nat → m Nat), f op 1 = pure 1
#[]
---
theorem
_private.temp.tmprjh7eosu.proof.0.f.match_1.eq_1
∀ (motive : Nat → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : Nat) → motive n.succ.succ),
  f.match_1 motive 0 h_1 h_2 h_3 = h_1 ()
#[]
Finished with no errors.

Second Theorem Proof:

theorem f_recursive (op : Nat → Nat → Id Nat) (n : Nat) : f op (n+2) =do {op (←  f op (n+1)) (←  f op n) }

:= by
  rw [f]

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmprjh7eosu/target2.olean
Finished imports
Finished replay
---
theorem
f_recursive
∀ (op : Nat → Nat → Id Nat) (n : Nat),
  f op (n + 2) = do
    let __do_lift ← f op (n + 1)
    let __do_lift_1 ← f op n
    op __do_lift __do_lift_1
#[sorryAx]
---
def
f
{m : Type → Type u_1} → [inst : Monad m] → (Nat → Nat → m Nat) → Nat → m Nat
:= fun {m : Type -> Type.{u_1}} [inst._@.temp.tmprjh7eosu.target2._hyg.7 : Monad.{0, u_1} m] (op : Nat -> Nat -> (m Nat)) (n : Nat) => sorryAx.{succ u_1} (m Nat) Bool.false
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmprjh7eosu/proof2.olean
Finished imports
Finished replay
---
def
f._sunfold
{m : Type → Type u_1} → [inst : Monad m] → (Nat → Nat → m Nat) → Nat → m Nat
:= fun {m : Type -> Type.{u_1}} [inst._@.temp.tmprjh7eosu.proof2._hyg.7 : Monad.{0, u_1} m] (op : Nat -> Nat -> (m Nat)) (n : Nat) => [mdata sunfoldMatch:1 f.match_1.{succ u_1} (fun (n._@.temp.tmprjh7eosu.proof2._hyg.26 : Nat) => m Nat) n (fun (_ : Unit) => [mdata sunfoldMatchAlt:1 Pure.pure.{0, u_1} m (Applicative.toPure.{0, u_1} m (Monad.toApplicative.{0, u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7)) Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))]) (fun (_ : Unit) => [mdata sunfoldMatchAlt:1 Pure.pure.{0, u_1} m (Applicative.toPure.{0, u_1} m (Monad.toApplicative.{0, u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7)) Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))]) (fun (n : Nat) => [mdata sunfoldMatchAlt:1 Bind.bind.{0, u_1} m (Monad.toBind.{0, u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7) Nat Nat (f.{u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7 op (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) (fun (__do_lift._@.temp.tmprjh7eosu.proof2._hyg.47.0 : Nat) => Bind.bind.{0, u_1} m (Monad.toBind.{0, u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7) Nat Nat (f.{u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7 op n) (fun (__do_lift._@.temp.tmprjh7eosu.proof2._hyg.47.1 : Nat) => op __do_lift._@.temp.tmprjh7eosu.proof2._hyg.47.0 __do_lift._@.temp.tmprjh7eosu.proof2._hyg.47.1))])]
#[]
---
theorem
_private.temp.tmprjh7eosu.proof2.0.f.match_1.eq_1
∀ (motive : Nat → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : Nat) → motive n.succ.succ),
  f.match_1 motive 0 h_1 h_2 h_3 = h_1 ()
#[]
---
def
f.match_1
(motive : Nat → Sort u_1) →
  (n : Nat) → (Unit → motive 0) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive n
:= fun (motive : Nat -> Sort.{u_1}) (n._@.temp.tmprjh7eosu.proof2._hyg.26 : Nat) (h_1 : Unit -> (motive (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))) (h_2 : Unit -> (motive (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) (h_3 : forall (n : Nat), motive (Nat.succ (Nat.succ n))) => Nat.casesOn.{u_1} (fun (x : Nat) => motive x) n._@.temp.tmprjh7eosu.proof2._hyg.26 (h_1 Unit.unit) (fun (n._@.temp.tmprjh7eosu.proof2._hyg.97 : Nat) => Nat.casesOn.{u_1} (fun (x : Nat) => motive (Nat.succ x)) n._@.temp.tmprjh7eosu.proof2._hyg.97 (h_2 Unit.unit) (fun (n._@.temp.tmprjh7eosu.proof2._hyg.98 : Nat) => h_3 n._@.temp.tmprjh7eosu.proof2._hyg.98))
#[]
---
theorem
_private.temp.tmprjh7eosu.proof2.0.f.match_1.eq_3
∀ (motive : Nat → Sort u_1) (n : Nat) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (n : Nat) → motive n.succ.succ), f.match_1 motive n.succ.succ h_1 h_2 h_3 = h_3 n
#[]
---
theorem
f.eq_3
∀ {m : Type → Type u_1} [inst : Monad m] (op : Nat → Nat → m Nat) (n_2 : Nat),
  f op n_2.succ.succ = do
    let __do_lift ← f op (n_2 + 1)
    let __do_lift_1 ← f op n_2
    op __do_lift __do_lift_1
#[]
---
theorem
f_recursive
∀ (op : Nat → Nat → Id Nat) (n : Nat),
  f op (n + 2) = do
    let __do_lift ← f op (n + 1)
    let __do_lift_1 ← f op n
    op __do_lift __do_lift_1
#[]
---
def
_private.temp.tmprjh7eosu.proof2.0.f.match_1.splitter
(motive : Nat → Sort u_1) → (n : Nat) → motive 0 → motive 1 → ((n : Nat) → motive n.succ.succ) → motive n
:= fun (motive : Nat -> Sort.{u_1}) (n._@.temp.tmprjh7eosu.proof2._hyg.26 : Nat) (h_1 : motive (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) (h_2 : motive (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (h_3 : forall (n : Nat), motive (Nat.succ (Nat.succ n))) => Nat.casesOn.{u_1} (fun (x : Nat) => motive x) n._@.temp.tmprjh7eosu.proof2._hyg.26 h_1 (fun (n._@.temp.tmprjh7eosu.proof2._hyg.97 : Nat) => Nat.casesOn.{u_1} (fun (x : Nat) => motive (Nat.succ x)) n._@.temp.tmprjh7eosu.proof2._hyg.97 h_2 (fun (n._@.temp.tmprjh7eosu.proof2._hyg.98 : Nat) => h_3 n._@.temp.tmprjh7eosu.proof2._hyg.98))
#[]
---
theorem
_private.temp.tmprjh7eosu.proof2.0.f.match_1.eq_2
∀ (motive : Nat → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : Nat) → motive n.succ.succ),
  f.match_1 motive 1 h_1 h_2 h_3 = h_2 ()
#[]
---
theorem
f.eq_1
∀ {m : Type → Type u_1} [inst : Monad m] (op : Nat → Nat → m Nat), f op 0 = pure 1
#[]
---
def
f
{m : Type → Type u_1} → [inst : Monad m] → (Nat → Nat → m Nat) → Nat → m Nat
:= fun {m : Type -> Type.{u_1}} [inst._@.temp.tmprjh7eosu.proof2._hyg.7 : Monad.{0, u_1} m] (op : Nat -> Nat -> (m Nat)) (n : Nat) => Nat.brecOn.{succ u_1} (fun (n : Nat) => m Nat) n (fun (n : Nat) (f_1 : Nat.below.{succ u_1} (fun (n : Nat) => m Nat) n) => f.match_1.{succ u_1} (fun (n._@.temp.tmprjh7eosu.proof2._hyg.26 : Nat) => (Nat.below.{succ u_1} (fun (n : Nat) => m Nat) n._@.temp.tmprjh7eosu.proof2._hyg.26) -> (m Nat)) n (fun ([anonymous] : Unit) (x._@.temp.tmprjh7eosu.proof2._hyg.99 : Nat.below.{succ u_1} (fun (n : Nat) => m Nat) (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) => Pure.pure.{0, u_1} m (Applicative.toPure.{0, u_1} m (Monad.toApplicative.{0, u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7)) Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (fun ([anonymous] : Unit) (x._@.temp.tmprjh7eosu.proof2._hyg.99 : Nat.below.{succ u_1} (fun (n : Nat) => m Nat) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => Pure.pure.{0, u_1} m (Applicative.toPure.{0, u_1} m (Monad.toApplicative.{0, u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7)) Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (fun (n : Nat) (x._@.temp.tmprjh7eosu.proof2._hyg.99 : Nat.below.{succ u_1} (fun (n : Nat) => m Nat) (Nat.succ (Nat.succ n))) => Bind.bind.{0, u_1} m (Monad.toBind.{0, u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7) Nat Nat x._@.temp.tmprjh7eosu.proof2._hyg.99.1 (fun (__do_lift._@.temp.tmprjh7eosu.proof2._hyg.47.0 : Nat) => Bind.bind.{0, u_1} m (Monad.toBind.{0, u_1} m inst._@.temp.tmprjh7eosu.proof2._hyg.7) Nat Nat x._@.temp.tmprjh7eosu.proof2._hyg.99.2.1 (fun (__do_lift._@.temp.tmprjh7eosu.proof2._hyg.47.1 : Nat) => op __do_lift._@.temp.tmprjh7eosu.proof2._hyg.47.0 __do_lift._@.temp.tmprjh7eosu.proof2._hyg.47.1))) f_1)
#[]
---
theorem
f.eq_2
∀ {m : Type → Type u_1} [inst : Monad m] (op : Nat → Nat → m Nat), f op 1 = pure 1
#[]
Finished with no errors.