KeenS

Require Import Arith.

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

KeenS

Goal forall P Q : nat -> Prop, P 0 -> (forall x , P x -> Q x) -> Q 0.
Proof.
  intros.
  apply H0.
  apply H.
Qed.

Goal forall P : nat -> Prop, P 2 -> (exists y, P (1 + y)).
Proof.
  intros.

KeenS

Require Import Arith.

Goal forall m n : nat, (n * 10) + m = (10 * n) + m.
Proof.
  intros.
  rewrite mult_comm.
  reflexivity.
Qed.

KeenS

Require Import Arith.

Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
  intros.
  rewrite (plus_assoc (n + m) p q).
  rewrite (plus_assoc (n + p) m q).
  rewrite <- (plus_assoc n m p).
  rewrite <- (plus_assoc n p m).
  rewrite (plus_comm m p).

KeenS

Require Import Arith.

Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
  intros.
  rewrite (plus_assoc (n + m) p q).
  rewrite (plus_assoc (n + p) m q).
  rewrite <- (plus_assoc n m p).
  rewrite <- (plus_assoc n p m).
  rewrite (plus_comm m p).

KeenS

Parameter G : Set.
Parameter mult : G -> G -> G.
Notation "x * y" := (mult x y).
Parameter one : G.
Notation "1" := one.
Parameter inv : G -> G.
Notation "/ x" := (inv x).

Axiom mult_assoc : forall x y z, x * (y * z) = (x * y) * z.
Axiom one_unit_l : forall x, 1 * x = x.

KeenS

Require Import Arith.

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

Goal forall n, sum_odd n = n * n.
Proof.

KeenS

(import (scheme base)
        (scheme time)
        (scheme write)
        (scheme file))

(define-syntax time
  (syntax-rules ()
    ((time form)
     (let ((start (current-jiffy)))
       form

KeenS

;; -*- coding: utf-8 -*-

(import (scheme base)
;        (scheme char)
        (scheme lazy)
        (scheme inexact)
;        (scheme complex)
        (scheme time)
        (scheme file)
;        (scheme read)

KeenS

(ql:quickload :parenscript)
(ql:quickload :cl-who)
(ql:quickload :clack)
(in-package :ps)
(defvar *canvas-id* "alien-canvas")
(clack:clackup
 (lambda (env)
   (list 200
         '(:content-type "text/html")
         (list