zvezdin (Aug 09 2020 at 08:15): zvezdin (Aug 09 2020 at 08:15):I am trying to prove properties of fixpoint functions. Upon given conditions, my function should return a result instead of an error. I have been researching tactics for a while now but couldn't find something that would unfold my computation.
As an example, assume the following function: https://pastebin.com/zkya3A0m
I am trying to prove this: https://pastebin.com/pHupqBiu
Yet my subgoal becomes this, which I don't know how to unfold: https://pastebin.com/tmcgb8qr
Will be very happy with any directions or tactics which might work here
Michael Soegtrop (Aug 09 2020 at 09:26):You need to rewrite with a lemma stating that eqb a a = true. You should read the documentation of Search in the reference manual to learn how you can search lemmas. And you possibly need to get a gut feeling on which modules you need to Require - note that Search doesn't find lemmas in modules you did not require.
Require Import NArith.
Definition maybe_return (A: Type) (a: nat) (b: nat) (d: A) :=
match (Nat.eqb a b) with
| true => Some d
| false => None
end.
Theorem test2: forall (a: nat) (c: Type), maybe_return _ a a c = Some c.
Proof.
intros.
simpl.
unfold maybe_return.
Search (Nat.eqb ?a ?a).
rewrite PeanoNat.Nat.eqb_refl.
reflexivity.
Qed.
Did you already go through the Software Foundations tutorial? It takes time to do so but there is no way around learning the things taught in this tutorial if you want to use Coq and following this tutorial might be the fastest way to learn this.
zvezdin (Aug 09 2020 at 14:26):Thank you for the thorough response and recommendations! This unblocked me in the meantime while I learn the rest of what Coq is about.
Last updated: Oct 13 2024 at 01:02 UTC