Deliberate.v

From mathcomp Require Import ssreflect.
Require Import List Nat Ensembles Image.
Import  ListNotations.


Notation empty := (Empty_set _).
Notation single := (Singleton _).
Notation union := (Union _).

Definition bigcup {T} (X : Ensemble (Ensemble T)) : Ensemble T :=
    fun x => exists I, In _ X I /\ In _ I x.

Definition bigcap {T} (X : Ensemble (Ensemble T)) : Ensemble T :=
    fun x => forall I, In _ X I -> In _ I x.

(************)
(* プログラム *)
(************)

(*
  L <- L_1, ... , L_n, not L_{n+1}, ... , L_{n+m}
  の形式の論理プログラムをルールと見做し、その集合をプログラムとしてる。
*)



Variable cons : Type.
Variable pred : Type.
Definition var := nat.

Inductive atom :=
  | vara : pred -> var -> atom
  | consa : pred -> cons -> atom.


Inductive literal :=
  | pos : atom -> literal
  | neg : atom -> literal.

Definition compl (l : literal) : literal :=
  match l with
  | pos a => neg a
  | neg a => pos a
  end.

Inductive rule :=
  | rule_intro : literal -> Ensemble literal -> Ensemble literal -> rule.

Definition head (c : rule) := let: rule_intro A _ _ := c in A.
Definition bodyp (c : rule) := let: rule_intro _ B _ := c in B.
Definition bodym (c : rule) := let: rule_intro _ _ C := c in C.

Definition program := Ensemble rule.




(************)
(* 基礎ルール *)
(************)
(*
  プログラムに現れる変数をエルブラン空間の要素で書き換えたもの全てからなる集合を基礎ルールとしてる
*)

Definition consOfAtom (a : atom) : Ensemble cons :=
  match a with
  | consa _ c => single c
  | _ => empty
  end.

Definition consOfLiteral (l : literal) : Ensemble cons :=
  match l with
  | pos a => consOfAtom a
  | neg a => consOfAtom a
  end.

Definition consOfLiterals (ls : Ensemble literal) : Ensemble cons :=
  bigcup (Im _ _ ls consOfLiteral).


Definition consOfRule (r : rule) : Ensemble cons :=
  let: rule_intro l ls1 ls2 := r in
  union (consOfLiteral l) (union (consOfLiterals ls1) (consOfLiterals ls2)).

Definition consOf (p : program) : Ensemble cons :=
  bigcup (Im _ _ p consOfRule).


(******)

Definition varOfAtom (a : atom) : Ensemble var :=
  match a with
  | vara _ v => single v
  | _ => empty
  end.

Definition varOfLiteral (l : literal) : Ensemble var :=
  match l with
  | pos a => varOfAtom a
  | neg a => varOfAtom a
  end.

Definition varOfLiterals (ls : Ensemble literal) : Ensemble var :=
  bigcup (Im _ _ ls varOfLiteral).

Definition varOfRule (r : rule) : Ensemble var :=
  let: rule_intro l ls1 ls2 := r in
  union (varOfLiteral l) (union (varOfLiterals ls1) (varOfLiterals ls2)).

Definition varOf (p : program) : Ensemble var :=
  bigcup (Im _ _ p varOfRule).


(******)


Definition substa (a : atom) (v : var) (c : cons) : atom :=
  match a with
  | vara p v' => if eqb v v' then consa p c else vara p v'
  | consa p c => consa p c
  end.

Definition substl v c (l : literal) : literal :=
   match l with
  | pos a => pos (substa a v c)
  | neg a => neg (substa a v c)
  end.

Definition substls (ls : Ensemble literal) v c : Ensemble literal :=
  Im _ _ ls (substl v c).


Definition substr  v c (r : rule): rule :=
  let: rule_intro l ls1 ls2 := r in
  rule_intro (substl v c l) (substls ls1 v c) (substls ls2 v c).

Definition subst (p : program) v c : program :=
  Im _ _ p (substr v c).


(******)


Definition base (p : program) : program :=
  let cons := consOf p in
  let vars := varOf p in
  fun r => exists c v, In _ cons c /\ In _ vars v /\  In _ (subst p v c) r.

Definition rules := list rule.

(*******)
(* 論証 *)
(*******)


Inductive arg (p : program) : rules -> Prop :=
  | arg0 : arg p []
  (* | arg1 rs r : arg p rs -> In r (base p) -> bodyp r  = [] -> arg p (r :: rs) *)
  | arg2 rs r : arg p rs -> In _  (base p) r ->
    (forall l, In _ (bodyp r) l -> (exists r', List.In r' rs /\ head r' = l )) -> arg p (r :: rs).


Definition claim (p : rules) : Ensemble literal :=
  match p with
  | [] => empty
  | r :: _ => single (head r)
  end.

Fixpoint concs (p : rules) : Ensemble literal :=
  match p with
  | [] => empty
  | r :: rs => union (single (head r)) (concs rs)
  end.


Fixpoint assms (p : rules) : Ensemble literal :=
  match p with
  | [] => empty
  | r :: rs => union (bodym r) (assms rs)
  end.

Inductive Arg p : Type :=
  | Arg_ rs : arg p rs -> Arg p.

Definition Claim {p} (a : Arg p) :=
  let: Arg_ p _ := a in claim p.

Definition Concs {p} (a : Arg p) :=
  let: Arg_ p _ := a in concs p.

Definition Assms {p} (a : Arg p) :=
  let: Arg_ p _ := a in assms p.

(***********)
(* 攻撃関係 *)
(***********)

Definition undercut {p} (A1 A2 : Arg p) :=
  exists l, In _ (Concs A1) l /\ In _ (Assms A2) l.

Definition rebuts {p} (A1 A2 : Arg p) :=
  exists l, In _ (Concs A1)  l/\ In _ (Concs A2) (compl l).

Definition Attack p := Arg p -> Arg p -> Prop.


(****************)
(*　セマンティック *)
(****************)
(*
  ここでは、議論の勝者を定義するのに特性関数の最小不動点を使ってる。
*)



Definition deffends {p} (x y : Attack p) (S : Ensemble (Arg p)) (A : Arg p) :=
  forall B, x B A -> exists C, In _ S C /\ y C B.


Definition F {p} (x y : Attack p) (S : Ensemble (Arg p)) : Ensemble (Arg p) :=
  fun A => deffends x y S A.


Theorem monotone {p} (x y : Attack p) S1 S2 :
  Included _ S1 S2 -> Included _ (F x y S1) (F x y S2).
Proof.
  move => H A.
  unfold In, F, deffends => H1 B.
  move /H1 => [C [HC CB]].
  exists C; split; auto.
Qed.

Fixpoint F_ {p} n (x y : Attack p) : Ensemble (Arg p):=
  match n with
  | 0 => F x y (Empty_set _)
  | S n' => F x y (F_ n' x y)
  end.

Definition lfp {p} (x y : Attack p) : Ensemble (Arg p):=
  fun A => exists n, In _ (F_ n x y) A.


(*******)
(* 熟議 *)
(*******)

(*
  熟議は、提案と法とvaluationを引数に取り真偽値を返す関数としている。
  提案は熟議の結果で真偽が判断される主張、
  法は論理プログラムで記述されたルールの集合、
  valuationは外部状態をあc意味する事を想定している。

  例えば、
    (罷免(x) <- 汚職(x)) ∈ low
  であるとする時、「政治家xが汚職をしたならば、xを罷免できる」を意味する法が存在する事を意味する。
    
 
  一方、fが意味するのは外部状態にまつわる命題のうち真になるものの集合である。
  つまり、'f 汚職 太郎' が真になる事は「環境fにおいて、太郎が汚職している事実が認められる」を意味する。
  
  また、factsはfをルールへ変換している。fが上記条件を満たす場合だと、
    (汚職(太郎) <-) ∈ facts f
  となる。
  
  そしてdeliberateは、lawとfacts f の和集合から、熟議フレームワークに基づいて論理的帰結を求めている。
  つまり、法に明記されたルールと、外部環境により判明する事実から、
    罷免(x) <- 汚職(x)
    汚職(太郎) <-
  を含むプログラムが得られ、その論理的帰結を求める。

*)

Definition valuation := pred -> cons -> Prop.

Definition facts (f : valuation) : program :=
  fun r => bodyp r = empty /\ bodym r = empty /\ exists p c, head r = pos (consa p c) /\ f p c.


Definition delibarate (propose : literal) (low : program) (f : valuation) :=
  let U := union low (facts f) in forall (x y : Attack U),
  exists r, In _ (lfp x y) r /\ Claim r = single (propose).