Logica-Lean

Esse repositório possui questões de dedução natural na lingaguem Lean, questões desenvolvidas para a disciplina de Lógica Computacional.

Link

Você poderá testar a corretude das questões no link abaixo que irá abrir o editor online lean com as respectivas questões resolvidas nesse repositório:

https://leanprover.github.io/live/3.3.0/#code=%0Asection%20%0A%0A--%20Questao%2062%20Logica%20proposicional%20:%20LCP-62%20%C2%ACA%20%E2%86%92%20B,%20%C2%ACB%20%E2%8A%A2%20A%0A%0Avariables%20A%20B:%20Prop%0A%0Aopen%20classical%0A%0Aexample%20(h1:%20%C2%AC%20A%20%E2%86%92%20B)%20(h2:%20%C2%AC%20B)%20:%20A%20:=%0A%20%20%20%20by_contradiction(%0A%20%20%20%20%20%20%20%20assume%20h3:%20%C2%AC%20A,%0A%20%20%20%20%20%20%20%20have%20h4:%20B,%0A%20%20%20%20%20%20%20%20%20%20%20%20from%20h1%20h3,%0A%20%20%20%20%20%20%20%20show%20false,%0A%20%20%20%20%20%20%20%20%20%20%20%20from%20h2%20h4)%09%0A%0Aend%0A%0Asection%0A%0A--%20Questao%2065%20Logica%20proposicional%20:%20LCP-65%20%20%C2%AC(A%E2%88%A7B),%20B%20%E2%8A%A2%20%C2%ACA%0A%0Avariables%20A%20B:%20Prop%0A%0A%0Aexample%20(h1:%20%C2%AC%20(A%20%E2%88%A7%20B))%20(h2:%20%20B)%20:%20%C2%AC%20A%20:=%0A%20%20%20%20%20%20%20%20assume%20h3:%20A,%0A%20%20%20%20%20%20%20%20have%20h4:%20A%20%E2%88%A7%20B,%0A%20%20%20%20%20%20%20%20%20%20%20%20from%20and.intro%20h3%20h2,%0A%20%20%20%20%20%20%20%20show%20false,%0A%20%20%20%20%20%20%20%20%20%20%20%20from%20h1%20h4%0A%0Aend%0A%0Asection%20%0A%0A--%20Questao%2035%20Logica%20proposicional%20:%20LCP%C2%AD35:%20(A%E2%86%92B)%20%E2%8A%A2%20((C%E2%88%A8A)%E2%86%92(B%E2%88%A8C))%0A%0Avariables%20A%20B%20C%20:%20Prop%0A%0Aexample%20(h1:%20A%20%E2%86%92%20B)%20:%20((C%E2%88%A8A)%E2%86%92(B%E2%88%A8C))%20:=%0A%20%20%20%20assume%20h2:%20(C%E2%88%A8A),%0A%20%20%20%20show%20(B%E2%88%A8C),%20from%20or.elim%20h2%0A%20%20%20%20%20%20%20%20(assume%20h3:%20C,%0A%20%20%20%20%20%20%20%20show%20B%20%E2%88%A8%20C,%20from%20or.inr%20h3)%0A%20%20%20%20%20%20%20%20(assume%20h4:%20A,%0A%20%20%20%20%20%20%20%20show%20B%20%E2%88%A8%20C,%20from%20or.inl%20(h1%20h4))%0A%0Aend%20%0A%0A%0Asection%20%0A%0A--%20Questao%2099%20Logica%20proposicional%20:%20LCP-99%20%C2%AC(%C2%ACA%E2%88%A7B%E2%88%A7%C2%ACC),%20B%20%E2%8A%A2%20(A%E2%88%A8C)%0A%0Aopen%20classical%0Avariables%20%7BA%20B%20C%20:%20Prop%7D%0A%0Alemma%20step1%20(h1%20:%20%C2%AC%20(A%20%E2%88%A8%20B))%20(h2%20:%20%C2%AC%20A)%20:%20%C2%AC%20A%20%E2%88%A7%20%C2%AC%20B%20:=%0Ahave%20h5:%20%C2%AC%20B,%20from%20(%0Aassume%20h3:%20B,%20%0Ahave%20h4:%20A%20%E2%88%A8%20B,%20%0Afrom%20or.inr%20h3,%0Ashow%20false,%0Afrom%20h1%20h4),%0Ashow%20%C2%AC%20A%20%E2%88%A7%20%C2%AC%20B,%20from%20and.intro%20h2%20h5%0A%0Alemma%20step2%20(h%E2%82%81%20:%20%C2%AC%20(A%20%E2%88%A8%20B))%20(h2%20:%20%C2%AC%20(%C2%AC%20A%20%E2%88%A7%20%C2%AC%20B))%20:%20false%20:=%0Ahave%20h3:%20A,%20from%0A%20%20(by_contradiction%20(assume%20h5:%20%C2%AC%20A,%0A%20%20%20%20have%20h6:%20%C2%AC%20A%20%E2%88%A7%20%C2%AC%20B,%20from%20step1%20h%E2%82%81%20h5,%0A%20%20%20%20show%20false,%20from%20h2%20h6)),%0Ahave%20h7:%20A%20%E2%88%A8%20B,%20from%20or.inl%20h3,%0Ashow%20false,%20from%20h%E2%82%81%20h7%0A%0Atheorem%20step3%20(h%20:%20%C2%AC%20(A%20%E2%88%A8%20B))%20:%20%C2%AC%20A%20%E2%88%A7%20%C2%AC%20B%20:=%0Aby_contradiction%0A%20%20(assume%20h'%20:%20%C2%AC%20(%C2%AC%20A%20%E2%88%A7%20%C2%AC%20B),%0A%20%20%20%20show%20false,%20from%20step2%20h%20h')%0A%0A%0Aexample%20(h1:%20%C2%AC(%C2%ACA%20%E2%88%A7%20B%20%E2%88%A7%20%C2%ACC))%20(h2:%20%20B)%20:%20A%20%E2%88%A8%20C%20:=%0A%20%20%20%20by_contradiction(%0A%20%20%20%20%20%20%20%20assume%20h3:%20%C2%AC%20(A%20%E2%88%A8%20C),%0A%20%20%20%20%20%20%20%20have%20h5:%20%C2%AC%20A%20%E2%88%A7%20%C2%AC%20C%20,%20%0A%20%20%20%20%20%20%20%20from%20step3%20h3,%20%0A%20%20%20%20%20%20%20%20have%20h7:%20%C2%AC%20A,%20from%20and.left%20h5,%0A%20%20%20%20%20%20%20%20have%20h8:%20%C2%AC%20C,%20from%20and.right%20h5,%0A%20%20%20%20%20%20%20%20have%20h11:%20B%20%E2%88%A7%20%C2%AC%20C%20,%20from%20and.intro%20h2%20h8,%0A%20%20%20%20%20%20%20%20have%20h4:%20%C2%AC%20A%20%E2%88%A7%20B%20%E2%88%A7%20%C2%AC%20C%20,%20from%20and.intro%20h7%20h11,%20%0A%20%20%20%20%20%20%20%20show%20false,%0A%20%20%20%20%20%20%20%20from%20h1%20h4%0A%20%20%20%20)%0A%0Aend%0A%0Asection%0A%0A--%20Questao%2028%20Logica%20de%20primeira%20ordem%20%20:%20%20%E2%88%80x,(R(x)%E2%86%94S(x))%20%E2%8A%A2%20%E2%88%83y,R(y)%E2%86%94%E2%88%83z,S(z)%0A%0Avariable%20U%20:%20Type%0Avariable%20R%20:%20U%20%E2%86%92%20Prop%0Avariable%20S%20:%20U%20%E2%86%92%20Prop%0A%0Aexample%20(h1:%20%E2%88%80%20x,%20(R%20x%20%20%E2%86%94%20S%20x))%20:%20(%E2%88%83y,R%20y)%20%E2%86%94%20(%E2%88%83z,S%20z)%20:=%0A%0Ashow%20(%E2%88%83y,R%20y)%20%E2%86%94%20(%E2%88%83z,%20S%20z),%20from%20iff.intro%0A%20%20(assume%20h%20:%20%E2%88%83y,R%20y,%0A%20%20%20%20show%20%E2%88%83z%20,S%20z,%20from%20exists.elim%20h%20(%0A%20%20%20%20assume%20(x%20:%20U)%20(hy:%20R%20x),%20%0A%20%20%20%20have%20h3:%20(R%20x%20%20%E2%86%94%20S%20x),%20from%20h1%20x,%0A%20%20%20%20have%20h4:%20S%20x,%20from%20iff.elim_left%20h3%20hy,%0A%20%20%20%20show%20%E2%88%83z%20,S%20z,%20from%20exists.intro%20x%20h4))%0A%20%20(assume%20h%20:%20%E2%88%83z,S%20z%20,%0A%20%20%20%20show%20%E2%88%83y,R%20y%20,%20from%20exists.elim%20h%20(%0A%20%20%20%20assume%20(x%20:%20U)%20(hy:%20S%20x),%20%0A%20%20%20%20have%20h3:%20(R%20x%20%20%E2%86%94%20S%20x),%20from%20h1%20x,%0A%20%20%20%20have%20h4:%20R%20x,%20from%20iff.elim_right%20h3%20hy,%0A%20%20%20%20show%20%E2%88%83z%20,R%20z,%20from%20exists.intro%20x%20h4))%0A%0Aend%20%0A%0Asection%0A%0A--%20Questao%2047%20Logica%20de%20primeira%20ordem%20%20:%20%20%E2%88%80x.(%E2%88%83y.P(y)%E2%86%92P(x))%20%E2%8A%A2%20%E2%88%80x.%E2%88%80y.(P(y)%E2%86%92P(x))%0A%20%20%20%0A%20%20%20%20variable%20U%20:%20Type%0A%20%20%20%20variable%20P%20:%20U%20%E2%86%92%20Prop%0A%0A%20%20%20%20example%20(h1%20:%20%E2%88%80%20x,((%E2%88%83%20y,%20P%20y)%20%E2%86%92%20P%20x))%20:%20%E2%88%80%20x,%20%E2%88%80%20y,(%20P%20y%20%E2%86%92%20P%20x)%20:=%0A%20%20%20%20assume%20a,%0A%20%20%20%20assume%20b,%20%0A%20%20%20%20assume%20h2:%20P%20b,%0A%20%20%20%20have%20h3:%20(%E2%88%83%20b,%20P%20b)%20%E2%86%92%20P%20a,%20from%20h1%20a%20,%0A%20%20%20%20have%20h4:%20%E2%88%83%20b,%20P%20b,%20from%20exists.intro%20b%20h2,%0A%20%20%20%20have%20h5:%20P%20a,%20from%20h3%20h4%20,%20%0A%20%20%20%20show%20P%20a,%20from%20h5%0A%20%20%0Aend%0A%0Asection%0A%0A--%20Questao%2013%20Logica%20de%20primeira%20ordem%20%20:%20%20%20%E2%88%80x.(P(x)%E2%86%94Q)%20%E2%8A%A2%20(%E2%88%80x.P(x))%E2%86%94Q%0A%0Avariables%20U%20Q:%20Prop%0Avariable%20P%20:%20U%20%E2%86%92%20Prop%0Avariable%20x:%20U%0A%0A%0Aexample%20(h1:%20(%E2%88%80%20x,(P%20x%20%E2%86%94%20Q)))%20:%20(%E2%88%80%20x,P%20x%20)%E2%86%94%20Q%20:=%0Ashow%20(%E2%88%80%20x,P%20x%20)%20%E2%86%94%20Q,%20from%20iff.intro%0A%20%20(assume%20h%20:%20%E2%88%80%20x,P%20x%20,%0A%20%20%20%20have%20h3:%20P%20x%20%E2%86%94%20Q,%20from%20h1%20x,%0A%20%20%20%20have%20h4%20:%20P%20x,%20from%20h%20x,%0A%20%20%20%20show%20Q,%20from%20iff.elim_left%20h3%20h4)%0A%20%20(assume%20h%20:%20Q%20,%0A%20%20%20%20assume%20y,%0A%20%20%20%20have%20h3:%20P%20x%20%E2%86%94%20Q,%20from%20h1%20x,%0A%20%20%20%20have%20h4:%20P%20x,%20from%20iff.elim_right%20h3%20h,%0A%20%20%20%20show%20P%20y%20%20,%20from%20h4)%0A%0Aend%0A%0Asection%0A%0A--%20Questao%2013%20Logica%20de%20primeira%20ordem%20:%20LCPO31%20%20%20P(i)%20%E2%8A%A2%20%C2%AC%E2%88%80x.%C2%ACP(x)%0A%0Avariable%20U:%20Prop%0Avariable%20P%20:%20U%20%E2%86%92%20Prop%0Avariables%20i%20x:%20U%0A%0A%0A--%20BEGIN%0A%0A%20%20example%20%20h1:%20P%20i%20%20:%20%C2%AC%E2%88%80%20x,%C2%AC%20P%20x%20:=%0A%20%20assume%20h%20:%20%E2%88%80%20x,%C2%AC%20P%20x%20,%0A%20%20show%20false,%20from%20(%0A%20%20%20%20have%20hi%20:%20%C2%AC%20P%20i,%20from%20h%20i,%0A%20%20%20%20show%20false,%20from%20hi%20h1)%0A%0A--%20END%0A%0A%0A%0Aend%0A%0Asection%0A%0A--%20Questao%20773%20dos%20desafios%20:%20%E2%8A%A2%20(((A%20%E2%86%92%20B)%20%E2%86%92%20((%E2%8A%A5%20%E2%86%92%20C)%20%E2%86%92%20D))%20%E2%86%92%20((D%20%E2%86%92%20A)%20%E2%86%92%20(E%20%E2%86%92%20(F%20%E2%86%92%20A))))%0A%0Aopen%20classical%0A%0Avariables%20A%20B%20C%20D%20E%20F:%20Prop%0A%0Aexample:%20((A%20%E2%86%92%20B)%20%E2%86%92%20((false%20%E2%86%92%20C)%20%E2%86%92%20D))%20%E2%86%92%20((D%20%E2%86%92%20A)%20%E2%86%92%20(E%20%E2%86%92%20(F%20%E2%86%92%20A)))%20%20:=%0A%20%20%20%20show%20(((A%20%E2%86%92%20B)%20%E2%86%92%20((false%20%E2%86%92%20C)%20%E2%86%92%20D))%20%E2%86%92%20((D%20%E2%86%92%20A)%20%E2%86%92%20(E%20%E2%86%92%20(F%20%E2%86%92%20A)))),%20from%20%0A%20%20%20%20(%0A%20%20%20%20%20%20%20%20assume%20h1:%20(A%20%E2%86%92%20B)%20%E2%86%92%20((false%20%E2%86%92%20C)%20%E2%86%92%20D),%0A%20%20%20%20%20%20%20%20show%20(D%20%E2%86%92%20A)%20%E2%86%92%20(E%20%E2%86%92%20(F%20%E2%86%92%20A)),%20from%20(%0A%20%20%20%20%20%20%20%20%20%20%20%20assume%20h2:%20(D%20%E2%86%92%20A),%20show%20%20(E%20%E2%86%92%20(F%20%E2%86%92%20A)),%20from%20(%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20assume%20h3:%20E,%20show%20(F%20%E2%86%92%20A),%20from%20(%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20assume%20h4:%20F,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20have%20hfalcd%20:%20(false%20%E2%86%92%20C)%20%E2%86%92%20D,%20from%20(%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20have%20hab%20:%20A%20%E2%86%92%20B,%20from%20(%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20assume%20ha%20:%20A,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20show%20B,%20from%20sorry%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20),%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20show%20(false%20%E2%86%92%20C)%20%E2%86%92%20D,%20from%20h1%20hab%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20),%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20have%20hfalc%20:%20false%20%E2%86%92%20C,%20from%20(%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20assume%20hfal%20:%20false,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20show%20C,%20from%20by_contradiction%20(%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20assume%20hnc%20:%20%C2%AC%20C,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20show%20false,%20from%20hfal%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20)%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20),%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20have%20hd%20:%20D,%20from%20hfalcd%20hfalc,%0A%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20show%20A,%20from%20h2%20hd%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20)%0A%20%20%20%20%20%20%20%20%20%20%20%20)%0A%20%20%20%20%20%20%20%20)%0A%20%20%20%20)%0Aend%0A%0Asection%0A%0A--%20Questao%20386%20dos%20desafios%20:%20((A%20%E2%86%92%20B)%20%E2%88%A7%20(C%20%E2%86%92%20D)),%20((B%20%E2%88%A8%20D)%20%E2%86%92%20E),%20(%C2%ACE)%20%E2%8A%A2%20%C2%AC(A%20%E2%88%A8%20C)%0A%0Avariables%20A%20B%20C%20D%20E:%20Prop%0A%0Aexample%20(h1:%20(A%20%E2%86%92%20B)%20%E2%88%A7%20(C%20%E2%86%92%20D))%20(h2:%20(B%20%E2%88%A8%20D)%20%E2%86%92%20E)%20(h4:%20%C2%ACE%20):%20%C2%AC(A%20%E2%88%A8%20C)%20:=%0A%20%20%20%20show%20%C2%AC(A%20%E2%88%A8%20C),%20from%20%0A%20%20%20%20(assume%20h:%20A%20%E2%88%A8%20C,%20show%20false,%20from%20or.elim%20h%20%0A%20%20%20%20%20%20%20%20(assume%20p1%20:%20A,%20show%20false,%20from%20%0A%20%20%20%20%20%20%20%20%20%20%20%20(have%20p2%20:%20A%20%E2%86%92%20B,%20from%20and.left%20h1,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20have%20p3%20:%20B,%20from%20p2%20p1,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20have%20p4%20:%20B%20%E2%88%A8%20D,%20from%20or.inl%20p3,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20have%20p5%20:%20E,%20from%20h2%20p4,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20show%20false,%20from%20h4%20p5%0A%20%20%20%20%20%20%20%20%20%20%20%20)%0A%20%20%20%20%20%20%20%20)%20%0A%20%20%20%20%20%20%20%20(assume%20p1%20:%20C,%20show%20false,%20from%20%0A%20%20%20%20%20%20%20%20%20%20%20%20(have%20p2%20:%20C%20%E2%86%92%20D,%20from%20and.right%20h1,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20have%20p3%20:%20D,%20from%20p2%20p1,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20have%20p4%20:%20B%20%E2%88%A8%20D,%20from%20or.inr%20p3,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20have%20p5%20:%20E,%20from%20h2%20p4,%0A%20%20%20%20%20%20%20%20%20%20%20%20%20show%20false,%20from%20h4%20p5%0A%20%20%20%20%20%20%20%20%20%20%20%20)%0A%20%20%20%20%20%20%20%20)%0A%20%20%20%20)%0A%0Aend%0A%0A