Problem with eval tactic

[NotBad4U]

I propose to open this issue to track the progress of the new eval tactic introduced in #1202.

The pull request proposed these changes:

• [x] find a way to handle idents and tactics taking idents as arguments (https://github.com/Deducteam/lambdapi/pull/1204)
• [ ] add a builtin "function" gen_id : String -> String that generates a string prefixed by the argument which is fresh within the context where it is used (useful for tactics taking fresh identifiers as argument like assume, set, have)
• [ ] allow eval in terms and rules too? (related to #217)

[NotBad4U]

I played with the eval tactic with the definitions in Tactic.lp.

This proof script cannot be unified.

symbol simp1 (x: τ nat) : π (x + 0 = x);
symbol simp2 (x: τ nat) : π (0 + x = x);

symbol lemma2 x: π ((0 + x) + 0 = x) ≔
begin
  assume x;
  //debug +u;

  // rewrite simp1; rewrite simp2; reflexivity;

  //eval (#rewrite simp1) & (#rewrite simp2) & #reflexivity; // Attempt 1: fail to unify
  //eval (2 * (#orelse (#rewrite simp1) (#rewrite simp2))) & #reflexivity; // Attempt 2: fail to unify
end;

It finishes with the error: [ℕ] and [Prop] are not unifiable. Unification goals are unsatisfiable.

The debug trace is

[unif] solve { recompute=false; metas={?7};
       to_solve=[τ nat → τ nat ≡ τ nat → Prop
                ;Prop ≡ τ nat
                ;Prop ≡ τ nat
                ;Prop ≡ τ nat
                ;Prop ≡ τ nat
                ;Prop ≡ ℕ
                ;Prop ≡ ℕ
                ;Prop ≡ τ nat];
       unsolved=[] }
[unif] solve τ nat → τ nat ≡ τ nat → Prop
[unif] decompose
[unif] add τ nat ≡ τ nat
[unif] add τ nat ≡ Prop
[unif] solve { recompute=false; metas={?7};
       to_solve=[τ nat ≡ Prop
                ;τ nat ≡ τ nat
                ;Prop ≡ τ nat
                ;Prop ≡ τ nat
                ;Prop ≡ τ nat
                ;Prop ≡ τ nat
                ;Prop ≡ ℕ
                ;Prop ≡ ℕ
                ;Prop ≡ τ nat];
       unsolved=[] }
[unif] solve τ nat ≡ Prop
[unif] whnf
[unif] solve ℕ ≡ Prop

I do not understand what makes the equation τ nat → τ nat ≡ τ nat → Prop introduced.

[fblanqui]

The 1st item has been done in https://github.com/Deducteam/lambdapi/pull/1215. The items 3 and 4 are not related to the eval tactic itself. Item 3 is related to #217. Item 4 is a proposal in the syntax but it would create too many problems. So we won't implement it a priori. So it actually remains item 2 only.

[NotBad4U]

Do we have a way to use the eval tactic on a proof that generates subgoals? For example, if we want to prove π (((⊤ = ⊤) ∨ (⊤ = ⊥)) ∧ ⊤), that will be nice for me to be able to create something such as

symbol bbt_wf (l: 𝕃 o) : Tactic;
rule bbt_wf □ ↪ #apply ⊤ᵢ
with bbt_wf (⊤ ⸬ $tl) ↪ #refine "∧ᵢ { apply ∨ᵢ₁; reflexivity } { bbt_wf $tl }"
with bbt_wf (⊥ ⸬ $tl) ↪ #refine "∧ᵢ { apply ∨ᵢ₂; reflexivity } { bbt_wf $tl }";

I recursively use ∧ᵢ, and then I apply the correct or introduction due to the head symbol and then refl. So I can use it like that:

symbol All [a] : (τ a → τ o) → 𝕃 a → τ o;
rule All _ □ ↪ ⊤
with All $p ($x ⸬ $l) ↪  ($p $x) ∧ (All $p $l);

symbol exemple: π (All (λ x, (x = ⊤) ∨ (x = ⊥)) (⊤ ⸬ ⊥ ⸬ ⊤ ⸬ □)) ≔
begin
eval bbt_wf (⊤ ⸬ ⊥ ⸬ ⊤ ⸬ □);
end;

[fblanqui]

Hi Alessio. This is currently not possible as it is formulated since #refine takes a term as argument and curly brackets are not part of the syntax of terms. You may however try to reformulate it to something like:

with bbt_wf (⊤ ⸬ $tl) ↪ #refine "∧ᵢ (∨ᵢ₁ (eq_refl _) _ " & bbt_wf $tl

[fblanqui]

Hi Alessio. Do you mind if I close this issue, which is not actually one? I prefer to reserve issues for actual and precise issues. You can use the Discussions tab instead.

[NotBad4U]

Yeah, np we can switch to the Discussion tab.