coq
Iris/Coq replacing literal
I am using Iris for Coq, but I am stuck on something.
Here, I want to get the snd value, l', from hd'. Then I can use IH with Hl and Hphi to finish the goal. Does anyone know how to replace hd' in the goal?
Solution
Your program (as in, the heap_lang code you are trying to verify) seems wrong. You are trying to get the second component of a location, which does not make sense, since locations are not pairs.
What your program should probably do here is load from the location, to get the pair that is stored in memory at location #hd'. In other words, instead of Snd #hd', it should be Snd (! #hd').
Once you fix your program, you can simply load from memory using wp_load. But this needs the load instruction (!) you are currently missing.
- How to make OCaml (or Coq) code from the llvmir code using vellvm framework
- Coq repeating "destruct" for disjunctive hypothesis causing unwanted destruction in the end
- Is there a lightweight way to define a mutable dictionary that can return all of its keys in Coq?
- Constructing proof terms inside a recursive function
- Coq notation defined inside a module expecting type without module prefix
- How does one implement Coq?
- Can a dependently typed language be Turing complete?
- Beta-reduction after delta-reduction in unfold tactic
- Equality for elements of sig type in Coq
- Defining mutually recursive types in Coq?
- How to mix sections with hints in Coq?
- Non-trivial Fixpoint on nested recursive types
- Is there an intuitionistic proof of `(A -> B \/ C) -> (A -> B) \/ (A -> C)`?
- InteractionTrees library - simple program on ASM
- What is the difference between Lemma and Theorem in Coq
- How to instruct `auto` to simplify the goal during proof search?
- Is is possible to rename a coq term?
- What are the practical limitations of a non-turing complete language like Coq?
- Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
- Is there a function that returns a list of values with specific type in OCaml?
- Formualting a logic in farmer astronaught
- What's the correct setup for Kami (Coq framework for Bluespec) to be able to run on WSL Ubuntu?
- Coq: keeping information in a match statement
- Showing polynomial equality in coq/ssreflect
- Syntax of the case tactic in coq
- Understanding nat_ind2 in Logical Foundations
- Split multiple conjuncts in the goal
- What `dependent induction` tactic does in Coq and how to use it
- Coq can't define an inductive proposition
- The `specialize` tatic in Coq does not work well with typeclasses?