;; The first three lines of this file were inserted by DrRacket. They record metadata
;; about the language level of this file in a form that our tools can easily process.
#reader(lib "htdp-advanced-reader.ss" "lang")((modname sol12) (read-case-sensitive #t) (teachpacks ((lib "valrose.rkt" "installed-teachpacks"))) (htdp-settings #(#t write mixed-fraction #t #t none #f ((lib "valrose.rkt" "installed-teachpacks")) #f)))
;;; sol12.rkt, PF1, Printemps 2009 (comme le temps passe...)
;;; Etudiant Niveau Avancé + teachpack valrose.rkt
;;; Le type abstrait FBF est intégré au teachpack valrose.rkt

(define (reformat fbf)          ; elimination des =>
  (if (atome? fbf) 
      fbf
      (local [(define r (connecteur fbf))]
        (case r
          ((non) (make-neg (reformat (arg1 fbf))))
          ((et ou) (make-fbf2 r (reformat (arg1 fbf)) (reformat (arg2 fbf))))
          (else (make-fbf2 'ou (make-neg (reformat (arg1 fbf))) (reformat (arg2 fbf))))))))

(show (reformat '((p => q) => p)))

(define (intersection? L1 L2)   ; au moins un element en commun ?
  (cond ((empty? L1) false)
        ((member (first L1) L2) true)
        (else (intersection? (rest L1) L2))))

(define (first-molecule Lfbf)    ; la premiere molecule d'une liste de fbf
  (cond ((empty? Lfbf) false)
        ((atome? (first Lfbf)) (first-molecule (rest Lfbf)))
        (else (first Lfbf))))

(show (first-molecule '(p q (non r) (p ou r))))
(show (first-molecule '(p q r)))

;(define (remove fbf Lfbf)
;  (cond ((empty? Lfbf) Lfbf)
;        ((equal? fbf (first Lfbf)) (rest Lfbf))
;        (else (cons (first Lfbf) (remove fbf (rest Lfbf))))))

(show (remove 'c '(a b c d c e)))

(define (add fbf Lfbf)
  (if (member fbf Lfbf) Lfbf (cons fbf Lfbf)))

"Wang algorithm"

(define (wang LHS RHS)        ; LHS et RHS sont des listes de fbf sans implications
  (if (intersection? LHS RHS) 
      true
      (local [(define fbf (first-molecule LHS))]   ; on cherche une molécule à gauche
        (if (not (equal? fbf false))
            (local [(define r (connecteur fbf))]
              (cond ((equal? r 'non) ; une negation a gauche
                     (wang (remove fbf LHS) (add (arg1 fbf) RHS)))
                    ((equal? r 'ou)  ; une disjonction a gauche
                     (and (wang (add (arg1 fbf) (remove fbf LHS)) RHS)
                          (wang (add (arg2 fbf) (remove fbf LHS)) RHS)))
                    ((equal? r 'et)  ; une conjonction a gauche
                     (wang (add (arg1 fbf) (add (arg2 fbf) (remove fbf LHS))) RHS))
                    (else (error 'wang "Bad syntax in fbf"))))
            (local [(define fbf (first-molecule RHS))]   ; on cherche une molécule à droite
              (if (not (equal? fbf false))
                  (local [(define r (connecteur fbf))]
                    (cond ((equal? r 'non) ; une negation a droite
                           (wang (add (arg1 fbf) LHS) (remove fbf RHS)))
                          ((equal? r 'ou)  ; une disjonction a droite
                           (wang LHS (add (arg1 fbf) (add (arg2 fbf) (remove fbf RHS)))))
                          ((equal? r 'et)  ; une conjonction a droite
                           (and (wang LHS (add (arg1 fbf) (remove fbf RHS)))
                                (wang LHS (add (arg2 fbf) (remove fbf RHS)))))
                          (else (error 'wang "Bad syntax in fbf"))))
                  false)))))) 

"Interactive prover"

(define (theoreme? fbf)
  (local [(define new-fbf (reformat fbf))]
        (begin (printf "*** J'essaye de prouver ~a\n" fbf)
               (printf "J'elimine d'abord les implications : ~a\n" new-fbf)
               (wang '() (list new-fbf)))))

(show (theoreme? '((p et (p => q)) => q)))
(show (theoreme? '((p => q) => p)))
(show (theoreme? '((p et (p => q)) => (p et q))))
(show (theoreme? '(p => (p et q))))
(show (theoreme? '(p => (p ou q))))
(show (theoreme? '(p => p)))
(show (theoreme? 'p))
(show (theoreme? '(q => (p ou ((non q) et p)))))
(show (theoreme? '(((p => (non q)) => q) => (p ou q))))

;;; BONUS

(define (prover-loop)
  (begin (printf "Give me a well-formed formula :\n")
         (local [(define fbf (read))]      ; lecture au clavier d'une formule sous forme de liste
           (if (member fbf '(stop bye quit exit fini ciao basta))
               (printf "Bye-bye.\n")
               (begin (printf "--> ~a\n" (if (theoreme? fbf) "It's a theorem !" "No, it's not a theorem."))
                      (prover-loop))))))

;(prover-loop)

;   p          true    false    true    false
;   q          true    true     false   false
;  nand(p,q)   false   true     true    true

(define (nand p q)
  (cond ((equal? q false) true)
        ((equal? p true) false)
        (else true))) 

(show (nand true true))
(show (nand true false)) 
(show (nand false true))
(show (nand false false))

(define ($not p)
  (nand p p))

(define ($and p q)
  ($not (nand p q)))

(define ($or p q)
  (nand ($not p) ($not q)))

(define (if-then-else p q r)
  ($or ($and p q) ($and ($not p) r)))            ; comporte > 4 portes nand 

(define (if-then-else-bis p q r)
  (nand (nand p  q)  (nand (nand  p  p)  r)))    ; comporte 4 portes nand

(define (evalb fbf AL)
  (if (atome? fbf)
      (if (boolean? fbf)
          fbf
          (local [(define try (assoc fbf AL))]
            (if (not (equal? try #f))
                (second try)
                (error 'evalb "Variable indefinie" fbf))))
      (local [(define op (connecteur fbf)) (define v1 (evalb (arg1 fbf) AL))]
        (cond ((equal? op 'non) (if (equal? v1 true) false true))
              ((equal? op 'et)  (if (equal? v1 false) false (evalb (arg2 fbf) AL)))
              ((equal? op 'ou)  (if (equal? v1 true) true (evalb (arg2 fbf) AL)))
              ((equal? op '=>)  (if (equal? v1 false) true (evalb (arg2 fbf) AL)))
              (else (error 'evalb "Mauvaise formule" fbf))))))

(show (evalb '(q => (p ou ((non q) et p))) '((p #t) (q #f))))

(define (union E1 E2)    ; union de deux ensembles (pas de repetition !)
  (cond ((empty? E1) E2)
        ((member (first E1) E2) (union (rest E1) E2))
        (else (cons (first E1) (union (rest E1) E2)))))

(show (union '(a z e r t y) '(r z h j k)))

(define (variables fbf)       ; l'ensemble des variables d'une fbf
  (cond ((atome? fbf) (if (symbol? fbf) (list fbf) empty))
        ((equal? 'non (connecteur fbf)) (variables (arg1 fbf)))
        (else (union (variables (arg1 fbf)) (variables (arg2 fbf))))))

(show (variables '(q => (p ou ((non (q ou r)) et p)))))

(define (gen-bools n)    ; retourne les 2^n listes de longueur n ne contenant que true et false 
  (if (= n 0)
      (list empty)
      (local [(define HR (gen-bools (- n 1)))]
        (append (map (lambda (L) (cons true L)) HR)
                (map (lambda (L) (cons false L)) HR)))))

(show (gen-bools 3))

(define (un-contre-exemple fbf)
  (local [(define vars (variables fbf))
          (define (iter L)
            (if (empty? L) 
                empty
                (local [(define test (map list vars (car L)))]
                  (if (evalb fbf test)
                      (iter (cdr L))
                      test))))]
    (iter (gen-bools (length vars)))))

(show (un-contre-exemple '(q => (p ou ((non q) et p)))))
(show (un-contre-exemple '(p => (q ou p))))

(define (new-theoreme? fbf)
  (empty? (un-contre-exemple fbf)))

(show (new-theoreme? '((p et (p => q)) => (p et q))))
(show (new-theoreme? '(p => (p et q))))
(show (new-theoreme? '(p => (p ou q))))
(show (new-theoreme? '(p => p)))
(show (new-theoreme? 'p))
(show (new-theoreme? '(q => (p ou ((non q) et p)))))
(show (new-theoreme? '(((p => (non q)) => q) => (p ou q))))