logic is silly

silly.rkt

#lang racket
(require redex)

(current-cache-all? #t)

(define-language L
  (e x t f (e ∧ e) (e ∨ e) (¬ e) (e → e))
  (x variable-not-otherwise-mentioned))

(define-extended-language LC L
  (C hole 
     (C ∧ e) (e ∧ C)
     (C ∨ e) (e ∨ C)
     (¬ C)
     (C → e)
     (e → C)))

(define R
  (reduction-relation 
   LC
   #:domain e
   ;; true and false
   (--> (in-hole C (e ∧ (¬ e)))
        (in-hole C f))
   (--> (in-hole C ((¬ e) ∧ e))
        (in-hole C f))
   (--> (in-hole C (e ∨ (¬ e)))
        (in-hole C t))
   (--> (in-hole C ((¬ e) ∨ e))
        (in-hole C t))
   (--> (in-hole C (e ∧ (¬ e)))
        (in-hole C f))
   (--> (in-hole C ((¬ e) ∧ (¬ e)))
        (in-hole C f))
   (--> (in-hole C ((¬ e) ∧ e))
        (in-hole C f))
   (--> (in-hole C ((¬ e) ∨ e))
        (in-hole C t))

   
   ;; commutitivity of and and or
   (--> (in-hole C (e_1 ∧ (e_2 ∧ e_3)))
        (in-hole C ((e_1 ∧ e_2) ∧ e_3)))
   (--> (in-hole C ((e_1 ∧ e_2) ∧ e_3))
        (in-hole C (e_1 ∧ (e_2 ∧ e_3))))
   #;(--> (in-hole C (e_1 ∨ (e_2 ∨ e_3)))
          (in-hole C ((e_1 ∨ e_2) ∨ e_3)))
   #;(--> (in-hole C ((e_1 ∨ e_2) ∨ e_3))
          (in-hole C (e_1 ∨ (e_2 ∨ e_3))))

   ;; double ands and ors
   (--> (in-hole C (e ∧ e))
        (in-hole C e))
   (--> (in-hole C (e ∨ e))
        (in-hole C e))

   ;; demorgan is silly
   (--> (in-hole C (¬ (e_1 ∧ e_2)))
        (in-hole C ((¬ e_1) ∨ (¬ e_2)))
        δ_∧)
   (--> (in-hole C (¬ (e_1 ∨ e_2)))
        (in-hole C ((¬ e_1) ∧ (¬ e_2)))
       δ_∨)

   ;; basics
   (-->  (in-hole C (¬ (¬ e_1)))
         (in-hole C e_1)
         ¬¬s)
      (--> (in-hole C (e_1 → e_2))
        (in-hole C ((¬ e_1) ∨ e_2))
        i)))

(apply-reduction-relation* R (term (¬ (¬ x))))
(apply-reduction-relation* R (term ((a ∨ (¬ b)) → ((c ∧ a) ∨ b))))