pathterminuspages/brkmnd.dk/aboutcontactabout me

Øvelser 1.2.1

Datalogi/Logic in Computer Science (Huth,Ryan)/Kapitel 1

Vis følgende udtryk.

De er løst i Coq. De kan faktisk direkte overføres til ProofWeb.

Require Import Classical. Variables p q r s t u : Prop. (* a *) Goal (p /\ q) /\ r -> s /\ t -> q /\ s. intro H. intro H0. split. apply H. apply H0. (* b *) Goal p /\ q -> q /\ p. intro H. split. apply H. apply H. (* c *) Goal (p /\ q) /\ r -> p /\ (q /\ r). intro H. split. apply H. split. apply H. apply H. (* d *) Goal (p -> (p -> q)) -> p -> q. intro H. intro H0. apply H. exact H0. exact H0. (* e *) Goal (q -> (p -> r)) -> ~r -> q -> ~p. intro H. intro H0. intro H1. intro. absurd r. exact H0. apply H. exact H1. exact H2. (* f *) Goal (p /\ q) -> p. intro H. apply H. (* g *) Goal p -> q -> (p /\ q). intro H. intro H1. split. exact H. exact H1. (* h *) Goal p -> (p -> q) -> q. intro H. intro H0. apply H0. exact H. (* i *) Goal (p -> q) /\ (q -> r) -> (p /\ q -> r). intro H. intro H0. apply H. apply H0. (* j *) Goal (q -> r) -> (p -> q) -> (p -> r). intro H. intro H0. intro H1. apply H. apply H0. apply H1. (* k *) Goal (p -> (q -> r)) -> (p -> q) -> p -> r. intro H. intro H0. intro H1. apply H. exact H1. apply H0. exact H1. (* l *) Goal (p -> q) -> (r -> s) -> p \/ q -> q \/ s. intro H. intro H1. intro H2. left. destruct H2. apply H. exact H0. exact H0. (* m *) Goal p \/ q -> r -> (p \/ q) /\ r. intro H. intro H0. split. exact H. exact H0. (* n *) Goal (p \/ (q -> p)) /\ q -> p. intro H. destruct H. destruct H. exact H. apply H. exact H0. (* o *) Goal (p -> q) -> (r -> s) -> p /\ r -> q /\ s. intro H. intro H0. intro H1. split. apply H. destruct H1. exact H1. apply H0. destruct H1. exact H2. (* p *) Goal (p -> q) -> ((p /\ q) -> p) /\ (p -> (p /\ q)). intro H. split. intro H0. destruct H0. exact H0. intro H0. split. exact H0. apply H. exact H0. (* q *) Goal q -> (p -> (p -> (q -> p))). intro H. intro H0. intro H1. intro H2. exact H1. (* r *) Goal (p -> q /\ r) -> (p -> q) /\ (p -> r). intro H. split. intro H0. apply H. exact H0. intro H0. apply H. exact H0. (* s *) Goal (p -> q) /\ (p -> r) -> p -> q /\ r. intro H. intro H0. split. destruct H. apply H. exact H0. destruct H. apply H1. exact H0. (* t *) Goal (p -> q) -> ((r -> s) -> (p /\ r -> q /\ s)). intro H. intro H0. intro H1. split. apply H. apply H1. apply H0. apply H1. (* u *) Goal (p -> q) -> ~q -> ~p. intro H. intro H0. intro. absurd q. exact H0. apply H. exact H1. (* v *) Goal p \/ (p /\ q) -> p. intro H. destruct H. exact H. apply H. (* w *) Goal r -> (p -> (r -> q)) -> p -> (q /\ r). intro H. intro H0. intro H1. split. apply H0. exact H1. exact H. exact H. (* x *) Goal (p -> (q \/ r)) -> (q -> s) -> (r -> s) -> p -> s. intro H. intro H0. intro H1. intro H2. destruct H. exact H2. apply H0. exact H. apply H1. exact H. (* y *) Goal (p /\ q) \/ (p /\ r) -> p /\ (q \/ r). intro H. split. destruct H. apply H. apply H. destruct H. left. apply H. right. apply H.