Stream: Coq users

Topic: solve by lia

pianke (Feb 17 2023 at 18:08):

H1: a>0
H2: a=0 (while a is natural number). I am unable to solve it by lia. What could be the reason?

Li-yao (Feb 17 2023 at 19:03):

what's the error message?

Laurent Théry (Feb 17 2023 at 20:10):

This works :

Laurent Théry (Feb 17 2023 at 20:11):

Require Import Lia.

Goal forall a, a>0 -> a=0 -> False.
intros H1 H2.
now lia.
Qed.

pianke (Feb 18 2023 at 11:32):

Directly apply lia. Not written in this way Goal forall a, a>0 -> a=0 -> False. Whats the difference between these ways?

pianke (Feb 18 2023 at 12:42):

(deleted)

Pierre Castéran (Feb 18 2023 at 14:10):

 @**pianke**

This was an answer to a part of of your previous post you moved later to another topic.

You may use the inversion tactic:

Require Import List Arith Lia.
Import ListNotations.

Goal forall (A:Type) (x: A), In x [] -> False.
Proof.
  intros A x H. inversion H.
Qed.

Goal forall (A:Type) (x y:A) l, In x (y::l) -> x = y \/ In x l.
Proof.
 intros A x y l H. inversion H.
 - left; congruence.
 - now right.
Qed.

Last updated: Oct 04 2023 at 19:01 UTC