Monad

[Scikud]

@spolu @jesse-michael-han lmk if these look alright

[jesse-michael-han]

Good, looks like the test for tac2 is passing. Can you write a similar test for tac3 and try to simulate the proof of the following using tac1, tac2, and tac3?

/--
  proves that 0 = 1 -> 0 = 2 by conjecturing that 0 = 1 -> false and then using false.elim
-/
example (h : 0 =  1) : 0 = 2 :=
begin
  have hf : false := nat.no_confusion h,
  exact false.elim ‹_›
end

[Scikud]

@spolu removed code for other tactics. Though we may possibly want to keep those around for the future since they potentially represent an alternative less dangerous way (but more tedious) way to do this.

--> Changed the endpoints to conjecture_assume and conjecture_add each just accept a conjecture string. Hypothesis name no longer required.

Using the example above, usage looks like for conjecture_add

["conjecture_add",["0","1","false"]]
{"error":null,"search_id":"0","tactic_state":"a b : ℝ,\th₀ : 0 < a ∧ 0 < b\t⊢ false","tactic_state_id":"2"}

and for conjecture_assume

["conjecture_assume",["0","1","false"]]
{"error":null,"search_id":"0","tactic_state":"a b : ℝ,\th₀ : 0 < a ∧ 0 < b,\th : false\t⊢ real.sqrt (a * b) ≤ (a + b) / 2","tactic_state_id":"3"}

lmk if that works :) !

[spolu]

This looks great. Let me try to run a few proof searches with each of these tactics to convince myself it does the right thing.

In particular given the checks we run once we reach the empty tactic state, does it actually work to close a proof search created from conjecture_add ? from conjecture_assume ?

[Scikud]

@spolu Two main changes: 1) The conjecture endpoints now return a new search id whenever they're called. 2) In order to make conjecturing play nice with finalize_proof When the endpoints are called they'll revert the all the hypothesis back into the goal, meaning you'll need to call "intros" again.

Example:

theorem dummy_test_theorem
  (x : ℝ)
  (y : ℝ) :
 (x + y = 2 * x) := sorry

Intros

["init_search",["dummy_test_theorem", ""]
{"error":null,"search_id":"0","tactic_state":"⊢ ∀ (x y : ℝ), x + y = 2 * x","tactic_state_id":"0"}

["run_tac",["0","0","intros"]]
{"error":null,"search_id":"0","tactic_state":"x y : ℝ\t⊢ x + y = 2 * x","tactic_state_id":"1"}

Using conjecture_assume (note search ID changes)

["conjecture_assume",["0","1","x = y"]]
{"error":null,"search_id":"1","tactic_state":"⊢ ∀ (x y : ℝ), x = y → x + y = 2 * x","tactic_state_id":"0"}

["run_tac",["1","0","intros"]]
{"error":null,"search_id":"1","tactic_state":"x y : ℝ,\th : x = y\t⊢ x + y = 2 * x","tactic_state_id":"1"}

Finish

["run_tac",["1","1","rw h"]]
{"error":null,"search_id":"1","tactic_state":"x y : ℝ,\th : x = y\t⊢ y + y = 2 * y","tactic_state_id":"2"}

["run_tac",["1","2","ring"]]
{"error":null,"search_id":"1","tactic_state":"no goals","tactic_state_id":"3"}

[spolu]

Fantastic!

What about the other one?

Out of curiosity? How come it reverts the hyps?

[spolu]

Also, based on your example above, do we need to intros first for the tactics to work?

[spolu]

@Scikud made a few aesthetics changes

This LGTM

r? @jesse-michael-han mind having a look?

[spolu]

@Scikud actually I also inlined the two tactics so that we have better error handling. Submitting an erroneous term will not crash the process anymore!

[spolu]

Example runs:

conjecture_set

["init_search", ["mathd_algebra_35", ""]]                                                                                                                
{"error":null,"search_id":"0","tactic_state":"⊢ ∀ (p q : ℝ → ℝ),\t(∀ (x : ℝ), p x = 2 - x ^ 2) → (∀ (x : ℝ), x ≠ 0 → q x = 6 / x) → p (q 2) = -7","tactic_state_id":"0"}
["run_tac",["0","0","intros"]]                                                                                                                                                                                                                                                                                     
{"error":null,"search_id":"0","tactic_state":"p q : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x\t⊢ p (q 2) = -7","tactic_state_id":"1"}                                                                                                                                          
["conjecture_set", ["0", "1", "q 2 = 3"]]
{"error":null,"search_id":"1","tactic_state":"p : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2\t⊢ ∀ (q : ℝ → ℝ), (∀ (x : ℝ), x ≠ 0 → q x = 6 / x) → q 2 = 3","tactic_state_id":"0"}                                                                                                                                     
["run_tac",["1","0","intros"]]                  
{"error":null,"search_id":"1","tactic_state":"p : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\tq : ℝ → ℝ,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x\t⊢ q 2 = 3","tactic_state_id":"1"}                                                                                                                                     
["run_tac",["1","1","rw [h]"]]           
{"error":"gen_tac_and_capture_res_failed: pos=(some ⟨1, 2⟩) msg=unknown identifier 'h'","search_id":null,"tactic_state":null,"tactic_state_id":null}     
["run_tac",["1","1","rw [h₁]"]]
{"error":null,"search_id":"1","tactic_state":"p : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\tq : ℝ → ℝ,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x\t⊢ 6 / 2 = 3\t\tp : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\tq : ℝ → ℝ,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x\t⊢ 2 ≠ 0","tactic_state_id":"2"}                         
["run_tac",["1","2","ring"]]                                                
{"error":null,"search_id":"1","tactic_state":"p : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\tq : ℝ → ℝ,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x\t⊢ 2 ≠ 0","tactic_state_id":"3"}                                                                                                                                       
["run_tac",["1","3","sorry"]]                              
{"error":"proof_validation_failed: msg=proof contains `sorry`","search_id":null,"tactic_state":null,"tactic_state_id":null}                              
["run_tac",["1","3","linarith"]]                                                                                                                                                                                                                                                                                   
{"error":null,"search_id":"1","tactic_state":"no goals","tactic_state_id":"4"}

conjecture_assume

["init_search", ["mathd_algebra_35", ""]]                                   
{"error":null,"search_id":"0","tactic_state":"⊢ ∀ (p q : ℝ → ℝ),\t(∀ (x : ℝ), p x = 2 - x ^ 2) → (∀ (x : ℝ), x ≠ 0 → q x = 6 / x) → p (q 2) = -7","tactic_state_id":"0"}                                                                                                                                           
["run_tac",["0","0","intros"]]                                                                                                                           
{"error":null,"search_id":"0","tactic_state":"p q : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x\t⊢ p (q 2) = -7","tactic_state_id":"1"}                                                                                                                                          
["conjecture_assume", ["0", "1", "q 2 = 3"]]                                                                                                             
{"error":null,"search_id":"1","tactic_state":"⊢ ∀ (p q : ℝ → ℝ),\t(∀ (x : ℝ), p x = 2 - x ^ 2) → (∀ (x : ℝ), x ≠ 0 → q x = 6 / x) → q 2 = 3 → p (q 2) = -7","tactic_state_id":"0"}                                                                                                                                 
["run_tac",["1","0","intros"]]                                                                                                                           
{"error":null,"search_id":"1","tactic_state":"p q : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x,\th : q 2 = 3\t⊢ p (q 2) = -7","tactic_state_id":"1"}                                                                                                                            
["run_tac",["1","1","rw [h]"]]                                                                                                                           
{"error":null,"search_id":"1","tactic_state":"p q : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x,\th : q 2 = 3\t⊢ p 3 = -7","tactic_state_id":"2"}                                                                                                                                
["run_tac",["1","2","ring"]]                                                                                                                             
{"error":"gen_tac_and_capture_res_failed: pos=(some ⟨1, 2⟩) msg=ring_nf failed to simplify","search_id":null,"tactic_state":null,"tactic_state_id":null}
["run_tac",["1","2","linarith"]]                                                                                                                         
{"error":"gen_tac_and_capture_res_failed: pos=(some ⟨1, 2⟩) msg=linarith failed to find a contradiction","search_id":null,"tactic_state":null,"tactic_state_id":null}                                                                                                                                              
["run_tac",["1","2","rw [h₀]"]]                                                                                                                          
{"error":null,"search_id":"1","tactic_state":"p q : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x,\th : q 2 = 3\t⊢ 2 - 3 ^ 2 = -7","tactic_state_id":"3"}                                                                                                                          
["run_tac",["1","3","ring"]]                                      
{"error":null,"search_id":"1","tactic_state":"no goals","tactic_state_id":"4"}

Good error handling

["init_search", ["mathd_algebra_35", ""]]
{"error":null,"search_id":"0","tactic_state":"⊢ ∀ (p q : ℝ → ℝ),\t(∀ (x : ℝ), p x = 2 - x ^ 2) → (∀ (x : ℝ), x ≠ 0 → q x = 6 / x) → p (q 2) = -7","tactic_state_id":"0"}
["run_tac",["0","0","intros"]]
{"error":null,"search_id":"0","tactic_state":"p q : ℝ → ℝ,\th₀ : ∀ (x : ℝ), p x = 2 - x ^ 2,\th₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x\t⊢ p (q 2) = -7","tactic_state_id":"1"}
["conjecture_assume", ["0", "1", "Z 2 = 3"]]
{"error":"conjecture_assume_have_failed: pos=(some ⟨1, 2⟩) msg=unknown identifier 'Z'","search_id":null,"tactic_state":null,"tactic_state_id":null}
["conjecture_assume", ["0", "1", "q 2 = 3"]]
{"error":null,"search_id":"1","tactic_state":"⊢ ∀ (p q : ℝ → ℝ),\t(∀ (x : ℝ), p x = 2 - x ^ 2) → (∀ (x : ℝ), x ≠ 0 → q x = 6 / x) → q 2 = 3 → p (q 2) = -7","tactic_state_id":"0"}

[jesse-michael-han]

There is something odd happening with proof validation when the conjectured statement does not refer to existing local constants. For example:

-- using theorem dummy_test_theorem
--  (x : ℝ)
--  (y : ℝ) :
-- (x + y = 2 * x) := sorry

["init_search", ["dummy_test_theorem",""]]
{"error":null,"search_id":"0","tactic_state":"⊢ ∀ (x y : ℝ), x + y = 2 * x","tactic_state_id":"0"}
["conjecture_assume", ["0", "0", "∀ (x y : ℝ), x + y = 2 * x"]]
{"error":null,"search_id":"1","tactic_state":"h : ∀ (x y : ℝ), x + y = 2 * x\t⊢ ∀ (x y : ℝ), x + y = 2 * x","tactic_state_id":"0"}
["run_tac", ["1", "0", "assumption"]]
{"error":"proof_validation_failed: msg=infer type failed, unknown variable\n  h","search_id":null,"tactic_state":null,"tactic_state_id":null}

[spolu]

@jesse-michael-han the commit above fixes the issue you pointed. Apparently we need to have hypotheses reverted for the proof finalization to known about their associated meta-variables.

We were calling revert_target_deps which would skip your hypothesis h here because it the target didn't depend on it.

According to the comment on revert_all:

/- Revert "all" hypotheses. Actually, the tactic only reverts
   hypotheses occurring after the last frozen local instance.
   Recall that frozen local instances cannot be reverted.
   We can use `unfreeze_local_instances` to workaround this limitation. -/

It is possible we may still have issues with frozen local instances, but I'm not sure what they are?

[jesse-michael-han]

LGTM, we can always prepend the revert by tactic.unfreeze_local_instances