0
$\begingroup$

I am working with two binary relations: g_o and pw_o, and I've defined pw_o below:

constants {A : Type} (g_o : A → A → Prop)

def pw_o (x y : A) : Prop := ∀ w : A, (g_o w x → g_o w y) ∧ (g_o y w → g_o x w)

I need to prove the following:

theorem prelim: ∀ x y z : A, g_o x y ∧ pw_o y z → g_o x z :=

I start with these tactics:

begin

   intros,

   cases a with h1 h2,

end

And I have this:

x y z : A,
h1 : g_o x y,
h2 : pw_o y z
⊢ g_o x z

Since pw_o is defined with a universal quantifier, I'd like to substitute w with x, then I would have (g_o x y → g_o x z) ∧ (g_o z x → g_o y x). After isolating the first conjunct with the "cases" tactic, I can use modus ponens on that first conjunct and h1. How can I tell Lean to replace w in the definition of pw_o with x and replace x and y in the definition of pw_o with y and z, respectively?

$\endgroup$
  • 1
    $\begingroup$ Questions on how to use particular tools are off-topic on this StackExchange. StackOverflow would be more appropriate. $\endgroup$ – Derek Elkins Mar 8 at 0:47
  • 1
    $\begingroup$ @DerekElkins We mostly seem to accept questions about Coq, so why not Lean? $\endgroup$ – David Richerby Mar 8 at 14:29
  • 1
    $\begingroup$ @DavidRicherby I don't have a problem with the specific reference to LEAN. (Personally, I'm anti-pseudo-code and would much prefer real code examples as long as they aren't too cluttered.) The problem is that the answer would need to be LEAN-specific. I would view a question like "what tactic do I need to use to perform universal instantiation in Coq" as just as off-topic for the same reasons. If questions like that about Coq aren't being treated as off-topic, that's a failure of community moderation in my mind. $\endgroup$ – Derek Elkins Mar 8 at 20:38
  • 1
    $\begingroup$ @DavidRicherby (contd.) Most of the Coq questions I've seen (and that I would consider on-topic) are really questions about proving things in constructive type theory in general and can and do get answers that are not Coq-specific, e.g. they use some other system such as Agda or just informal type theory. Some LEAN-specific questions would be fine. Questions about LEAN rather than how to use it. For example, "what differences are there between the metatheory implemented by LEAN versus CIC?" $\endgroup$ – Derek Elkins Mar 8 at 20:38
0
$\begingroup$

I've found an answer to the question I've posed. Here are the tactics I've used:

begin
   unfold pw_o,
   intros,
   cases a with h1 h2,
   let h3 : A := x,
   let h4 : (g_o x y → g_o x z) ∧ (g_o z x → g_o y x) := h2 x,
   apply (h4.left h1),
end

I've unfolded pw_o to make the universal quantifier explicit. After I've isolated pw_o y z as a hypothesis, I've replaced all occurrences of w with x. Since h4.left is a function from g_o x y to g_o x z, I've applied it to h1, which is a term of g_o x y, to obtain a term of g_o x z, which was the ultimate goal.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.