Stream: Coq users

Topic: Performing computations in proofs

view this post on Zulip 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:
I am trying to prove this:
Yet my subgoal becomes this, which I don't know how to unfold:

Will be very happy with any directions or tactics which might work here

view this post on Zulip 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

Theorem test2: forall (a: nat) (c: Type), maybe_return _ a a c = Some c.
unfold maybe_return.
Search (Nat.eqb ?a ?a).
rewrite PeanoNat.Nat.eqb_refl.

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.

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC