autotaker

{-# LANGUAGE MultiParamTypeClasses,FlexibleInstances,FunctionalDependencies ,UndecidableInstances#-}

data Pair a b = Pair a b
data Zero = Zero
data Succ a = Succ a

class Tuple t n c | t n -> c where
    nth :: t -> n -> c

instance Tuple (Pair a b) Zero a where

autotaker

import Data.List
import Data.Char
import Control.Monad

data Expr = Number Int | Op Char
instance Show Expr where
    show (Number x) = show x
    show (Op ch) = [ch]

type Ops a = [(a -> a -> [a], Char )]

autotaker

Require Import Arith.
Theorem FF : ~exists f, forall n, f (f n) = S n.
Proof.
intro.
destruct H.
remember (x 0) as y.
assert( forall k, x (y + k) = S k ).
induction k.
rewrite <- (plus_n_O y).
rewrite Heqy.

autotaker

Require Import Arith.

Inductive Tree : Set := | Node : list Tree -> Tree.

Require Import Max.
Require Import List.
Fixpoint depth (a : Tree) :nat :=  
match a with
| Node l => 
(fix f (l : list Tree) : nat := match l with | nil => 0 | x :: xs => max (depth x+1) (f xs) end) l end.

autotaker

Require Import Arith.

(* Q6 *)
Goal forall x y, x < y -> x + 10 < y + 10.
  Proof.
  intros.
  apply plus_lt_compat_r.
  apply H.
  Qed.

autotaker

(* Q11 *)
Require Import Arith.

Fixpoint sum_odd(n:nat) : nat :=
  match n with
  | O => O
  | S m => 1 + m + m + sum_odd m
end.

Goal forall n, sum_odd n = n * n.

autotaker

(* Q13 *)
Inductive pos : Set :=
  | S0 : pos
  | S : pos -> pos.

Fixpoint plus(n m:pos) : pos := 
  match n with
    | S0 => S m
    | S n => S (plus n m)
  end.

autotaker

(* Q16 *)
Definition tautology : forall P : Prop, P -> P := 
  fun (P : Prop) (H : P) => H.


Definition Modus_tollens : 
  forall P Q : Prop, ~Q /\ (P -> Q) -> ~P :=
  fun (P Q : Prop) (H : ~ Q /\ (P -> Q)) =>
    match H with
    | conj nq p2q => (fun p => nq (p2q p))

autotaker

Parameter A : Set.
Definition Eq (a : A) (b : A) :  Prop :=
  forall (f : A -> Prop), f a <-> f b.

Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
intros.
split.
intro.
unfold Eq in H.

autotaker

Require Import Coq.Logic.Classical.
Lemma ABC_iff_iff :
  forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
  intros.
  split.
  intro.
  split.
  intro.
  split.