Brontekst bekijken van Beweren en bewijzen/de zuilen/Zekerheid/5. Natuurlijke deductie/predikaatlogica stellingen

<noinclude>{{BenB/Inhoud}}</noinclude>{{Literatuur|...}}
{{opvallend|1=Met de guest login van de [http://prover.cs.ru.nl/ Coq web interface] staan er al een aantal opgaven. '''Let op: ''' de opgaven in predicaatlogica gebruiken echter een andere syntax! Gebruik daarom de opgaven uit deze werkplaats en voeg <code>Require Import BenB.</code>, het domein <code>Variable D: Set.</code>, en declaraties van predicaten toe, bv. <code>Variable R : D -> D -> B.</code>.

Je kunt de uitwerkingen niet opslaan, dat zul je even zelf moeten doen in een tekstbestandje. De opgaven kun je zowel met Coq oefenen als op papier. Uiteraard zijn de opgaven in Coq vorm gegeven, dus zonder aannames, zie [[Beweren en bewijzen/de opzet/gereedschap/Coq|de uitleg bij Coq]].

Op deze pagina kan men elkaar helpen met de opgaven.

'''N.b.:''' bij een aantal opgaven zul je een doel als '''a=a''' moeten bewijzen. Dit is triviaal waar en je kunt het bewijzen met behulp van het commando '''lin_solve'''.

'''N.b.:''' aan het einde staan een aantal oefenopgaven die gebruik maken van '''Hypothesis'''. Een hypothese is gewoon een extra bewering in je aannames, maar Coq verbergt deze. Stel je hebt de hypothese '''Domain''' en een tak van het bewijs is exact hetzelfde geworden als deze hypothese, dan kan men de tak in Coq afsluiten met '''exact Domain.'''
}}

{{BenB/!|Jasper Berendsen||De formules hier onder hebben soms te veel haakjes. Ga zelf na wat er qua haakjes mis is aan een formule.}}

<source lang="coq">
Theorem exercise_003 : (forall x : D, forall y : D, R x y -> ~ R y x) -> (forall x : D, ~ R x x). (* medium *)
Theorem exercise_004 : (forall x : D, forall y : D, R x y) -> (forall x : D, R x x). (* easy *)
Theorem exercise_005 : ((exists x : D, P x) -> (forall y : D, Q y)) -> (forall x : D, forall y : D, (P x -> Q y)). (* medium *)
Theorem exercise_006 : (forall x : D, P x -> Q x) /\ (exists x : D, P x) -> (exists x : D, Q x). (* medium *)
Theorem exercise_007 : ~(forall x : D, P x \/ Q x) -> ~(forall x : D, P x). (* easy *)
Theorem exercise_008 : ~(forall x : D, P x) -> ~(forall x : D, P x /\ Q x). (* easy *)
Theorem exercise_009 : (forall x : D, P x /\ Q x) -> ~(exists x : D, ~ P x). (* medium *)
Theorem exercise_010 : (exists x : D, P x -> Q x) -> (forall x : D, P x) -> (exists x : D, Q x). (* medium *)
Theorem exercise_011 : (forall x : D, P x -> Q x) /\ ~(exists x : D, Q x) -> (forall x : D, ~ P x). (* medium *)
Theorem exercise_012 : (forall x : D, (exists y : D, R y x) -> P x) -> (exists x : D, exists y : D, R x y) -> (exists x : D, P x). (* medium *)
Theorem exercise_013 : (exists x : D, P x \/ Q x) -> (forall x : D, ~ Q x) -> (exists x : D, P x). (* medium *)
Theorem exercise_014 : ~(forall x : D, exists y : D, R x y) -> ~(forall x : D, R x x). (* easy *)
Theorem exercise_015 : ~(forall x : D, P x \/ (Q x -> T x)) -> ~(forall x : D, T x). (* easy *)
Theorem exercise_016 : (forall x : D, P x \/ R x x) -> (forall x : D, P x -> (exists y : D, R x y /\ R y x)) -> forall x : D, exists y : D, R x y. (* difficult *)
Theorem exercise_017 : ~(exists x : D, forall y : D, (R y x -> ~ R x y) /\ (~ R x y -> R y x)). (* deze opgave is wat onnatuurlijk *) (* difficult *)
Theorem exercise_018 : (exists x : D, P x) \/ (exists x : D, Q x) -> (exists x : D, P x \/ Q x). (* difficult *)
Theorem exercise_019 : (exists x : D, P x \/ Q x) -> (exists x : D, P x) \/ (exists x : D, Q x). (* medium *)
Theorem exercise_020 : (exists x : D, P x /\ Q x) -> (exists x : D, P x) /\ (exists x : D, Q x). (* medium *)
Theorem exercise_021 : ~((forall x : D, P x) /\ (exists x : D, ~ P x)). (* medium *)
Theorem exercise_022 : (exists x : D, R x x /\ P x) -> ~ (forall x : D, P x -> ~ (exists y : D, R x y)). (* medium *)
Theorem exercise_023 : ((exists x : D, P x) -> (forall x : D, Q x)) -> (forall y : D, P y -> Q y). (* easy *)
Theorem exercise_024 : (exists x : D, ~(P x \/ Q x)) -> ~(forall x : D, P x). (* medium *)
Theorem exercise_025 : ~(forall x : D, P x /\ Q x) /\ (forall x : D, P x) -> ~(forall x : D, Q x). (* medium *)
Theorem exercise_026 : (forall x : D, R x x -> Q x) /\ (exists x : D, forall y : D, R x y) -> (exists x : D, Q x). (* medium *)
Theorem exercise_027 : (forall x : D, P x \/ Q x) -> (forall x : D, ~ P x -> Q x). (* medium *)
Theorem exercise_028 : (forall x : D, forall y : D, R x y) -> ~(exists x : D, ~ R x x). (* medium *)
Theorem exercise_029 : forall y : D, (exists x : D, (P y -> Q x)) -> (P y -> (exists x : D, Q x)). (* medium *)
Theorem exercise_030 : (exists x : D, P x \/ Q x) /\ (forall x : D, ~ Q x) -> (exists x : D, P x). (* medium *)
Theorem exercise_031 : (forall x : D, P x /\ Q x) -> (forall x : D, P x \/ (exists y : D, R x y)). (* easy *)
Theorem exercise_032 : (forall x : D, P x /\ ~ Q x -> S x) /\ (exists x : D, ~ S x /\ ~ Q x) -> (exists x : D, ~ P x). (* medium *)
Theorem exercise_033 : (exists x : D, ~ (P x \/ Q x)) -> ~ (forall x : D, P x).
Theorem exercise_034 : ~(forall x : D, P x \/ (Q x -> S x)) -> ~(forall x : D, S x). (* easy *)
Theorem exercise_035 : (forall y : D, Q y -> ~ exists x : D, P x) /\ (forall x : D, P x) -> (forall y : D, ~ Q y). (* medium *)
Theorem exercise_036 : (exists x : D, forall y : D, ~ R x y) -> ~ (forall x : D, R x x). (* medium *)
Theorem exercise_037 : (forall x : D, P x) \/ (forall x : D, Q x) -> (forall x : D, P x \/ Q x). (* medium *)
Theorem exercise_038 : (exists x : D, x = x) -> (forall x : D, P x \/ Q x) -> ~ (forall x : D, ~ P x /\ ~ Q x). (*is exists x : D, x = x nodig? Gebruik command lin_solve om een doel a=a op te lossen.*) (* difficult *)
Theorem exercise_039 : ~ (exists x : D, P x \/ Q x) -> (forall x : D, ~ P x /\ ~ Q x). (* medium *)
Theorem exercise_040 : (forall x : D, forall y : D, R x y \/ R y x) -> (forall x : D, R x x). (* medium *)
Theorem exercise_041 : (forall x : D, forall y : D, R x y -> R y x) /\ (forall x : D, exists y : D, R x y) -> (forall x : D, exists y : D, R y x). (* medium *)
Theorem exercise_042 : (exists x : D, P x \/ Q x) /\ ~(exists x : D, P x) -> ~(forall x : D, Q x -> P x). (* difficult *)
Theorem exercise_043 : (exists x : D, P x -> Q x) /\ (forall x : D, ~(P x /\ Q x)) -> (exists x : D, ~ P x). (* medium *)
Theorem exercise_044 : (forall x : D, P x -> Q x) /\ (forall x : D, ~(P x /\ Q x)) -> (forall x : D, ~ P x). (* medium *)
Theorem exercise_045 : ((exists x : D, P x) -> (forall x : D, Q x)) -> (forall x : D, P x -> Q x). (* easy *)
Theorem exercise_046 : (exists x : D, P x -> A) -> (forall x : D, P x) -> A. (* medium *)
Theorem exercise_047 : (forall x : D, P x -> A) -> (exists x : D, P x) -> A. (* medium *)
Theorem exercise_048 : (forall x : D, forall y : D, R x y /\ R y x) -> ~(exists x : D, ~ R x x). (* medium *)
Theorem exercise_049 : (forall y : D, P y -> (forall x : D, R x y)) -> (exists y : D, P y) -> (exists z : D, forall x : D, R x z). (* medium *)
Theorem exercise_050 : (forall y : D, P y -> (forall x : D, R x y)) -> (forall x : D, P x) -> (forall x : D, forall y : D, R x y).(* medium *)
Theorem exercise_051 : (forall x : D, (exists y : D, R x y) -> P x) /\ (forall x : D, R x x) -> (forall z : D, P z). (* medium *)
Theorem exercise_052 : (exists y : D, forall x : D, P x -> R x y) -> (forall x : D, P x -> (exists y : D, R x y)). (* medium *)
Theorem exercise_053 : (forall x : D, ~ P x -> Q x) /\ (exists y : D, ~ Q y) -> (exists y : D, P y). (* medium *)

Variable a : D. Theorem exercise_054 : (forall x : D, (exists y : D, R x y) -> R x a) -> (forall z : D, ~ R z a -> (forall y : D, ~ R z y)). (* medium *)

Theorem exercise_055 : ~(forall x : D, P x /\ Q x) /\ (forall x : D, Q x) -> ~(forall x : D, P x). (* medium *)
Theorem exercise_056 : (forall x : D, P x -> (forall y : D, R y x)) -> ~(exists x : D, P x /\ ~ R x x). (* difficult *)
Theorem exercise_057 : (forall x : D, forall y : D, ~ R x y -> R y x) -> (forall x : D, R x x). (* medium *)
Variable a : D. Variable b : D. Theorem exercise_058 : (forall x : D, forall y : D, x = y) /\ (P a) -> (P b). (* medium *)
Theorem exercise_059 : (forall x : D, forall y : D, x = y) -> (exists x : D, P x) -> (forall x : D, P x). (* medium *)
Variable a : D. Variable b : D. Theorem exercise_060 : (P b) /\ ~ (P a) -> ~(forall x : D, forall y : D, x = y). (* medium *)
Theorem exercise_061 : (exists x : D, ~ R x x) -> (exists x : D, exists y : D, ~ R x y). (* easy *)
Theorem exercise_062 : (forall x : D, ~exists y : D, R x y) -> (forall x : D, forall y : D, ~ R x y). (* easy *)
(* Disjunction_implies_existence *)
Variable a : D. Variable b : D. Variable c : D. Theorem exercise_063 : (P a \/ P b \/ P c) -> (exists x : D, P x). (* medium *)
Theorem exercise_067 : (forall x : D, ~ P x) -> ~ (exists x : D, P x). (* medium *)
Theorem exercise_068 : ~ (exists x : D, P x) -> (forall x : D, ~ P x). (* easy *)
Theorem exercise_069 : (exists x : D, ~ P x) -> ~ (forall x : D, P x).
Theorem exercise_070 : ~ (forall x : D, P x) -> (exists x : D, ~ P x). (* easy *)
Theorem exercise_071 : forall x : D, x = x. (* easy *)
Theorem exercise_072 : (exists x : D, P x) -> (exists x : D, x=x).
Theorem exercise_073 : (exists x : D, exists y : D, R x y) -> (exists x : D, x=x).
Theorem exercise_077 : (exists x : D, forall y : D, P x \/ P y) -> (exists x : D, P x). (* medium *)
Theorem exercise_082 : (forall x : D, P x) -> (forall x y z : D, P x /\ P y /\ P z). (* medium *)
Theorem exercise_084 : (exists x : D, (P x /\ Q x)) -> (exists x : D, P x) /\ (exists x : D, Q x) .
Theorem exercise_085 : forall x : D, forall y : D, forall z : D, x = y /\ y = z -> x = z. (* easy *)
Theorem exercise_086 : forall x:D, P x -> (exists y : D, P y). (* easy *)


(* On a finite domain, existence implies a disjunction
   over different elements; this is less trivial *)
Hypothesis Domain : exists x1 : D, exists x2 : D, exists x3 : D,
  (forall x : D, (x = x1 \/ x = x2 \/ x = x3)) /\
  ~(x1 = x2) /\ ~(x1 = x3) /\ ~(x2 = x3).
Hypothesis P_holds : exists x : D, P x.
Theorem exercise_065 : exists x1 : D, exists x2 : D, exists x3 : D, (P x1 \/ P x2 \/ P x3) /\ ~(x1 = x2)
  /\ ~(x1 = x3) /\ ~(x2 = x3). (* difficult *)

(* This theorem shows that on a domain of at most two elements,
   any instantation of three variables will have a duplicate.
   Try the same for a domain of three elements, if you have
   a spare afternoon, the length of the proof explodes with
   the number of elements of D.
*)
Hypothesis Domain : exists x1 : D, exists x2 : D, forall x : D,
  (x = x1 \/ x = x2).
Theorem exercise_066 : forall x1 : D, forall x2 : D, forall x3 : D, (x1=x2 \/ x1=x3 \/ x2=x3). (* difficult *)

(* A universal statement does not carry existential import,
   but if we know the domain is not empty : D, then we can
   prove that universal predication implies singular
   predication of a property P *)
Hypothesis Domain : exists x1 : D, exists x2 : D, exists x3 : D,
  forall x : D, (x = x1 \/ x = x2 \/ x = x3).
Theorem exercise_074 : (forall x : D, P x) -> (exists x : D, P x).

Hypothesis Domain : exists x1 : D, exists x2 : D, exists x3 : D,
  forall x : D, (x = x1 \/ x = x2 \/ x = x3).
Theorem exercise_075 : (forall x : D, forall y : D, P x \/ P y) -> (exists x : D, P x). (* difficult *)

Hypothesis Domain : exists x1 : D, exists x2 : D, exists x3 : D,
  forall x : D, (x = x1 \/ x = x2 \/ x = x3).
Theorem exercise_076 : (forall x : D, exists y : D, P x \/ P y) -> (exists x : D, P x). (* difficult *)

(* This theorem shows that if we have a transitive
   relation on a 3-element set, and if each element has
   a successor, then some element must be reflexive for
   this relation *)
Hypothesis Domain : exists x1 : D, exists x2 : D, exists x3 : D,
  forall x : D, (x = x1 \/ x = x2 \/ x = x3).
Hypothesis Successor : forall x : D, exists y : D, R x y.
Hypothesis Transitive : forall x y z : D, ((R x y /\ R y z) -> R x z).
Theorem exercise_078 : exists x : D, R x x. (* challenge *)

(* The following theorem shows that under the assumption
   that our domain has 3 elements, if a property holds
   for 3 different elements, it holds for all elements.
   Because the cases that have to be considered multiply : D,
   the proof takes almost 400 lines. This is a good
   demonstration of how primitive first-order logic can be.
*)
Hypothesis Domain : exists x1 : D, exists x2 : D, exists x3 : D,
  forall x : D, (x = x1 \/ x = x2 \/ x = x3).
Theorem exercise_079 : (exists x : D, exists y : D, exists z: D, P x /\ P y /\ P z /\ ~(x = y) /\ ~(x = z) /\ ~(y = z)) -> (forall x : D, P x). (* challenge *)

Variable a : D. Variable b : D. Variable c : D.
Hypothesis Domain : forall x : D, (x = a \/ x = b \/ x = c).
Theorem exercise_080 : (forall x : D, P x) -> (P a /\ P b /\ P c). (* medium *)

Variable a : D. Variable b : D. Variable c : D.
Hypothesis Domain : forall x : D, (x = a \/ x = b \/ x = c).
Theorem exercise_081 : (P a /\ P b /\ P c) -> (forall x : D, P x). (* difficult *)

Hypothesis R_symmetric : forall x y : D, R x y -> R y x.
Hypothesis R_transitive : forall x y z : D, (R x y /\ R y z -> R x z).
Theorem exercise_083 : forall x : D, (exists y : D, R x y) -> R x x. (* difficult *)
</source>