Email Gateway (Aug 18 2022 at 10:26): Email Gateway (Aug 18 2022 at 10:26):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Here I have a simple goal and tactic:
Goal "j <= (i :: nat) --> k < j --> i - j + k < i"
Level 0 (1 subgoal)
j <= i --> k < j --> i - j + k < i
1. j <= i --> k < j --> i - j + k < i
val it = [] : Thm.thm list
by (induct_tac "i" 1);
Level 1 (2 subgoals)
j <= i --> k < j --> i - j + k < i
1. j <= 0 --> k < j --> 0 - j + k < 0
2. !!n. j <= n --> k < j --> n - j + k < n
==> j <= Suc n --> k < j --> Suc n - j + k < Suc n
val it = () : unit
but trying to convert the same proof into Isar I get
lemma mpl_lem [rule_format] : "j <= (i :: nat) --> k < j --> i - j + k
< i" ;
proof (prove): step 0
goal (1 subgoal):
1. j <= i --> k < j --> i - j + k < i
variables:
i, j, k :: nat
apply (induct_tac "i" 1) ;
proof (prove): step 0
goal (1 subgoal):
1. j <= i --> k < j --> i - j + k < i
variables:
i, j, k :: nat
*** Type unification failed: Clash of types "nat" and "fun"
*** Cannot meet type constraint:
*** Term: (i::nat) :: nat
*** Type: nat => bool
*** At command "apply" (line 428 of stdin).
Does anyone have any ideas about what might be happening here?
Thanks for any help
Jeremy
Email Gateway (Aug 18 2022 at 10:26):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Jeremy,
In ML style, the following command says to perform induction on the variable
"i" in subgoal 1:
by (induct_tac "i" 1);
If you want to specify a subgoal number in Isar style, you need to use the
square-bracket syntax:
apply (induct_tac [1] "i")
You can also use e.g. [2-4] to specify a range of subgoals, or [!] to specify
all subgoals. The same syntax is used to specify subgoals with case_tac,
rule_tac, etc.
Usually you won't need to specify a number, and it will default to the first
subgoal:
apply (induct_tac "i")
When you apply (induct_tac "i" 1) in Isar, I'm not sure exactly how it gets
interpreted; my best guess is that it is parsed as an application of the term
"i" to the term "1", which doesn't type check because "i" is not a function.
Last updated: May 03 2024 at 12:27 UTC