DS-Prover

API Usage

import requests
base_url = 'https://smlab.niser.ac.in/project/ds-prover/'

Generating tactics:

data = {'goal' : 'm n : ℕ\n⊢ m + n = n + m',
        'num_samples' : 8,       # number of tactics to be generated (2 - 99)
        'model' : 'default'}     # model to be used ('default' or 'augmented')

response = requests.post(base_url + 'generate/', json=data)
print(response.json())
# Output: {'tactics': [['rw nat.add_comm', -2.579533815383911], ['rw [nat.add_comm, nat.add_left_comm]', -2.5869863033294678], ['rw add_comm', -2.908726453781128], ['simp', -3.146678924560547], ['rw [nat.add_comm n m, nat.add_comm n m]', -3.509650945663452], ['simp [nat.add_comm]', -3.6089301109313965], ['intros', -3.636415958404541], ['apply nat.add_left_cancel', -3.760629177093506]], 'time': 0.6610127680469304}

Proving statements:

data = {'statement' : 'example (m n : ℕ) : m + n = n + m :=',
        'model' : 'default',     # model to be used ('default' or 'augmented')
        'sampling' : 'fixed'}    # sampling method ('fixed' or 'dynamic')

response = requests.post(base_url + 'prove/', json=data)
print(response.json())
# Output: {'proof': ['rw nat.add_comm'], 'proved': 1, 'statement': 'import all\nexample (m n : ℕ) : m + n = n + m :=', 'time': 11.5}

Additional Examples to Try:

def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂
def non_increasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≥ f x₂

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : non_decreasing (g ∘ f) :=

---

example {a b c : ℝ} (hab : a ≤ b) : c + a ≤ c + b :=

---

example (a b c : ℝ) : (a * b) * c = b * (a * c) :=

---

variables x y z w : ℕ

example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w :=

---

theorem de_morgan_disj : ∀ (P Q : Prop), ¬(P ∨ Q) → ¬P ∧ ¬Q :=

---

def even_fun (f : ℝ → ℝ) := ∀ x, f (-x) = f x
def odd_fun (f : ℝ → ℝ) := ∀ x, f (-x) = -f x

example (f g : ℝ → ℝ) : even_fun f → even_fun g →  even_fun (f + g) :=