0

I've been working through Volume 1 of Software Foundations, and I can't get past a pair of optional questions in Logic.v. Anyone have any idea what to do?

Theorem leb_plus_exists : forall n m, n <=? m = true -> exists x, m = n+x. Proof. Admitted.

Theorem plus_exists_leb : forall n m, (exists x, m = n+x) -> n <=? m = true. Proof. (* FILL IN HERE *) Admitted.

I simple cannot get past intros in the first question. I am completely stumped on what to do.

asked Jan 29, 2024 at 9:19

1 Answer 1

1

Please be aware that solutions to exercises in Software Foundations, especially volume 1: Logical Foundations, are not to be published.

So, here is a hint: do induction n before you do intros m, which keeps all statements general in m.

Or, not necessary here, but if you do all intros first, then you need generalize dependent m: see generalize dependent.

answered Jan 29, 2024 at 10:47
Sign up to request clarification or add additional context in comments.

Comments

Your Answer

Draft saved
Draft discarded

Sign up or log in

Sign up using Google
Sign up using Email and Password

Post as a guest

Required, but never shown

Post as a guest

Required, but never shown

By clicking "Post Your Answer", you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.