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
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.
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: Sep 26 2023 at 12:02 UTC