Zulip Chat Archive

Stream: new members

Topic: Composite and DeMorgan


view this post on Zulip Debendro Mookerjee (Mar 20 2020 at 16:35):

Here are two definitions and a theorem:

def dvd (m n: ): Prop :=  k, n = m * k
def prime (p : ) : Prop := p  2   n, dvd n p  n = 1  n = p
def composite (d : ): Prop:= ¬ prime d

theorem composite_fact (c: ) : composite c   (a b: ), c = a*b  a  b  b < c:=
begin
    split,
    rw composite,
    rw prime,
end

this is the tactic state:

2 goals
c : 
 ¬(c  2   (n : ), dvd n c  n = 1  n = c)  ( (a b : ), c = a * b  a  b  b < c)

c : 
 ( (a b : ), c = a * b  a  b  b < c)  composite c

In the first goal, how do I use DeMorgan's law to foil out the not in the first goals?

view this post on Zulip Anne Baanen (Mar 20 2020 at 16:41):

I think the law you're looking for is not_and. A trick for finding rewriting suggestions: the tactic squeeze_simp reports the lemmas that simp can apply


Last updated: May 11 2021 at 14:11 UTC