proof,isabelle,theorem-proving,isar , Skip a subgoal while proving in Isabelle
Skip a subgoal while proving in Isabelle
Question:
Tag: proof,isabelle,theorem-proving,isar
I am trying to prove a theorem but got stuck at a subgoal (that I prefer to skip and prove later). How can I skip this and prove the others ?
First, I tried oops and sorry but they both abort the entire proof (instead of the only subgoal). I also tried to put the subgoal into a dummy lemma (assuming proven with sorry) then using it (apply (rule [my dummy lemma])) but it applies the dummy lemma to every other subgoals (not only the first one).
Answer:
It mostly depends on whether you are using the archaic (sorry for that ;)) apply-style or proper structured Isar for proving. I will give a small example to cover both styles. Assume you wanted to prove
lemma "A & B"
Where A and B just serve as placeholders for potentially huge formulas.
As structured proof you would do something like:
proof
show "A" sorry
next
show "B" sorry
qed
I.e., in this style you can use sorry to omit proofs for subgoals.
In apply-style you could do
apply (rule conjI)
defer -- "moves the first subgoal to the last position"
apply (*proof for subgoal "B"*)
apply (*proof for subgoal "A"*)
There is also the apply-style command prefer n which moves subgoal n to the front.
Related:
isabelle
I'm reading the Isabelle tutorial and been trying to clear my concept on use of primrec and fun. With what I've searched so far, including the answer here; I understand that constructor inside primrec can have only one equation and primrec has [simp] by default whereas fun can have multiple...
haskell,proof,induction
I have the following: elem :: Eq a => a -> [a] -> Bool elem _ [] = False elem x (y:ys) = x == y || elem x ys How can I prove that for all x's y's and z's... elem z (xs ++ ys) == elem z xs...
isabelle
I have found that I can prove the following lemma, which seems false to me. lemma assumes "∀a b. f a > f b ∧ a ≠ b" shows "∀a b. f b > f a" using assms by auto How can the lemma above be true? Is Isabelle substituting...
set,higher-order-functions,isabelle,theorem-proving,isar
I would like to create a quotient type with quotient_type in Isabelle/HOL in which I would left "non-constructed" the non-empty set S and the equivalence relation ≡. The goal is for me to derive generic properties w.r.t. S and ≡ over the quotient-lifted set S/≡. In this way, it would...
isabelle,isar
I am trying to prove a big case distinction in Isabelle for some (conceptually) simple arithmetic statement. During the proof, I stumbled upon the following subgoal. ⋀d l k. 0 < d ⟹ ¬ 2 * k + 1 ≤ 2 * l ⟹ 2 * l ≠ 1 ⟹...
isabelle
This is a derivative question of Existing constants (e.g. constructors) in type class instantiations. The short question is this: How can I prevent the error that occurs due to free_constructors, so that I can combine the two theories that I include below. I've been sitting on this for months. The...
isabelle
How can I convert a set to a list in Isabelle? I am interested in a function definition, with the signature: "'a set => 'a list" How can I define this?...
sml,ml,isabelle
This question is related to how sectioning and Sidekick can be used with Isabelle/ML in Isabelle/jEdit. Consider two Isar commands, section and ML. These commands act as sectioning commands in the tree of the jEdit Sidekick plugin. One consequence is that I can use multiple ML{*...*} statements in a THY...
loops,logic,proof,turing-machines,halting-problem
For instance, let's say I have this Turing machine, H, which tells us whether or not a program and input will halt. Let's say we call H on itself. It has to give an answer, so if it prints out "does not halt" then didn't it technically halt to print...
recursion,isabelle,theorem-proving
The problem I am wondering if is there a natural way of encoding in Isabelle a grammar like this: type_synonym Var = string datatype Value = VInt int | ... datatype Cmd = Skip | NonDeterministicChoice "Cmd set" | ... The motivation would be to give definition a few specification...
solver,isabelle,theorem-proving
Every goal that I have encountered in Isabelle so far that could be solved using arith could also be solved by presburger and vice versa, for example lemma "odd (n::nat) ⟹ Suc (2 * (n div 2)) = n" by presburger (* or arith *) What's the difference between the...
coq,proof,dependent-type
As an exercise in Coq, I'm trying to prove that the following function returns a pair of lists of equal length. Require Import List. Fixpoint split (A B:Set)(x:list (A*B)) : (list A)*(list B) := match x with |nil => (nil, nil) |cons (a,b) x1 => let (ta, tb) := split...
isabelle
I can prove the following lemma: lemma lem1: assumes "(a::real) ≤ b / c" and "c > 0" shows "a * c ≤ b" using assms using pos_le_divide_eq[of "c" "a" "b"] by auto however, if I use bound variables, the proof does not work. lemma lem2: assumes "∀a b c....
isabelle
I figure out how to modify some Isar and ML, but here I don't know how to get what I want. I use declare and using to turn info on and off, like with these (and other longer combinations): declare[[simp_trace_new mode=full]] declare[[show_sorts=false]] using[[simp_trace_new mode=full]] using[[show_sorts=false]] I've created jEdit macros to...
math,proof,prime-factoring,number-theory
According to topcoder Link, We need to compute till square root of number to list its all prime factors... Now I am able to prove in the following code that we are doing right till we are in the for loop.. But I am unable to figure out why the...
isabelle
In many paper proofs you see authors substitute variables in equations. For example, if there is an inequality "f(x-y) >= g(x-y)*z, the author simply writes let h=(x-y), therefore "f(h) >= g(h)*z" and continues with the proof. To do the same in Isabelle, would I have to assume that h=(x-y), is...
isabelle
I want to prove the following lemma lemma assumes "f (w+n) - f w / n ≤ g (w+n)" shows "∀n. (f (w+n) - f w) / n ≤ g (w+n)" I assumed this would be very simple however it is proving trickier than I first thought. From my thoughts,...
isabelle
Is it possible to define using the Isabelle proof assistant a theory involving functions of variable arity ? For example, I would like to define the theory of all predicates of arity n, which are invariant by cyclic permutation. Given a type T and an integer n, I would like...
haskell,undefined,proof
How could one prove that the following is true for every list xs: undefined ++ xs = undefined ...
coq,isabelle
I would like to be able use something like de Bruijn indices in Isabelle or in Coq, in order to refer to variables that have been introduced by quantifiers. For example, instead of writing: forall x. forall y. (p x y) I would like to write something like: forall x....
coq,isabelle,type-parameter
I started learning Isabelle and wanted to try defining a monoid in Isabelle but don't know how. In Coq, I would do something like this: Inductive monoid (τ : Type) (op: τ -> τ -> τ) (i: τ): Prop := | axioms: (forall (e: τ), op e i = e)...
isabelle
Given the function f: definition f :: "real => real" where "f x = x" I can show that as n tends to 0, f(x+n) tends to f(x) by the following lemma lemma "(λn. f(x+n)) -- 0 --> f x" unfolding f_def apply (auto intro!: tendsto_eq_intros) done As a further...
proof,isabelle,theorem-proving,isar
I am trying to prove a theorem but got stuck at a subgoal (that I prefer to skip and prove later). How can I skip this and prove the others ? First, I tried oops and sorry but they both abort the entire proof (instead of the only subgoal). I...
algorithm,list,ocaml,proof
With a given positive integer list and the addition and the multiplication as operators, I want to compute the highest value. So if my list is [2,3,4], it will be : 2 * 3 * 4 = 24. If there is at least one 1 in the list, it is...
solver,isabelle,theorem-proving
In Isabelle, I often find that I can prove a goal successfully using different solvers. Generally I would prefer to use the weakest solver that can just about prove the goal. Based on my experience with Isabelle so far, my current understanding is that in order of increasing strength and...
algorithm,fibonacci,proof
I need to formal proof that below algorithm return 1 for n = 1 and 0 in other cases. function K( n: word): word; begin if (n < 2) then K := n else K := K(n − 1) * K(n − 2); end; Anyone could help? Thank you...
isabelle
I am attempting to use the fundamental theorem of calculus to prove the lemma lm1: lemma lm1: fixes f :: "real ⇒ real" assumes "∀x∈{a..b}. (f has_vector_derivative f' x) (at x within {a .. b})" "∀x∈{a..b}. a ≤ x" "∀x∈{a..b}. x ≤ b" shows "∀x∈{a..b}. (f' has_integral (f x -...
coq,proof,coqide
I want to prove this : 1 subgoals x : nat y : nat z : nat ______________________________________(1/1) x + y - z = x + (y - z) It looks trivial, but it confuse me a lot, and I need it for another proof. Thanks....
coq,proof,coqide
(BEq a a0 = BTrue \/ BEq a a0 = BFalse) is either true or false since a==a0 or a!=a0. However, I'm not sure how I can get Coq to see this. Here is my complete proof window: 4 subgoal a : aexp a0 : aexp st : state ______________________________________(1/4)...
locale,record,isabelle,interpretation
Using the Algebra library, I encountered the following problem. In a proof I wanted to interpret the additive structure of a ring as a group. Here is a sample code: theory aaa imports "~~/src/HOL/Algebra/Ring" begin lemma assumes "ring R" shows "True" proof- interpret ring R by fact interpret additive: comm_group...
pattern-matching,proof,agda,dependent-type
I have some experience using Coq and am now in the process of learning Agda. I'm working on a correctness proof of insertion sort and have reached a point where I would like to perform something similar to Coq's rewrite tactic. Currently, I have: open import Data.Nat open import Relation.Binary.PropositionalEquality...
isabelle
I would like to use the simplifier to replace subterms that are not equalities. Instead of a generic definition of my problem, I will illustrate this by an example: Say I have a simple programming language and a Hoare logic on top of it. Say we have if, while, and...
isabelle
I have proven this simp rule: lemma AAA: the_sector (log_update ?f ?s) ?p = the_sector ?s ?p The rule is not used to simplify the following: lemma BBB: "(λA. if A then (the_sector (log_update f s) p) else B) = (λA. if A then (the_sector s p) else B)" I...
isabelle
I have been working with limits and topology in and I want to prove the following lemma: lemma fixes f g :: "real ⇒ real" assumes "open S" "∀a b. a < b <--> f a < f b" "∀a. (f a)>0" "continuous_on UNIV (f)" "∀w∈S. ∀h. (w+h)∈S --> h...
algorithm,asymptotic-complexity,proof,growth-rate
I have been asked to prove or disprove the following conjecture: For any given constant c>0 | If f(n) = O(h(n)) then c*f(n) = O(h(n)) I have came up with the following counter example: Let f(n) = n and c = n+1. Then c*f(n) = (n+1)n = n^2+n = O(n^2),...
proof,agda,idris,proof-of-correctness,isar
Most proof assistants are functional programming languages with dependent types. They can proof programs/algorithms. I'm interested, instead, in proof assistant suitable best for mathematics and only (calculus for instance). Can you recommend one? I heard about Mizar but I don’t like that the source code is closed, but if it...
coq,proof
Just like the title says, I'm looking for a way to prove st X + st Y = st Y + (st X - 1) + 1 in Coq. I've been trying applying various combinations of plus_comm, plus_assoc and plus_permute but I haven't been able to make it go through....
merge,proof,array-algorithms
Prove that it is enough to make at most 5 comparisons in order to merge two sorted sequences of lengths 2 and 5.
algorithm,time-complexity,proof,dht,kademlia
I'm now learning Kademlia network by reading the classical paper Kademlia: A Peer-to-peer Information System Based on the XOR Metric. I want to understand the complexity of its operation but still cannot figure it out. In the 3 Sketch of proof section, the paper gives two definitions: Depth of a...
typeclass,isabelle
Consider this Isabelle code theory Scratch imports Main begin datatype Expr = Const nat | Plus Expr Expr it is quite reasonable to instantiate the plus type class to get nice syntax for the Plus constructor: instantiation Expr :: plus begin definition "plus_Exp = Plus" instance.. end But now, +...
isabelle
expect to use the subgoal to run the list which defined by let? aa = [1,2] and run rev_app on this aa and show the value as [2,1] theory Scratch2 imports Datatype begin datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) (* This is...
algorithm,asymptotic-complexity,proof,growth-rate
I need to prove or disprove the following conjecture: if f(n) = O(h(n)) AND g(n) = O(k(n)) then (f − g)(n) = O(h(n) − k(n)) I am aware of the sum and product theorems for growth combination, but I could not find a way to apply them here, even though...
algorithm,asymptotic-complexity,proof,growth-rate
I was asked to prove or disprove the following conjecture: n^2 = Ω(nlogn) This one feels like it should be very easy, and intuitively it seems to me that because Ω is a lower bound function, and n^2 is by definition of higher magnitude than nlogn, then it is also...
logic,proof,logic-programming,first-order-logic
For any given logic program, proof theory of it uses SLD (Selective Linear Definite) resolution to find the satisfiablity of the query. For the same logic program, we can apply fixed point theorem to find the models. My question is, should we consider finding fixed point of logic programs as...
isabelle
I have looked into the Isabelle tutorial which presents an example of it's use in verifying security protocol. However, it is a bit out of my understanding as I only know the basics. I'm looking for some examples which are not just simple theorems but practical applications using Isabelle/HOL. For...
isabelle
I have a term in mind, say "foo 1 2 a b", and I'd like to know if Isabelle can simplify it for me. I'd like to write something like simplify "foo 1 2 a b" and have the simplified term printed in the output buffer. Is this possible? My...