Veracity Logic Mechanised in Coq

By Daniel Britten and Steve Reeves.

This Coq formalisation is an attempt to mechanise a logic for veracity, with the goal of precisely pinning down the meaning of veracity. Veracity is concerned with trust, truth, demonstrability and authenticity. We take an approach inspired by intuitionistic logic, in part due to a desire not to "lose information" as proofs progress. For further details, please see the arXiv paper "A logic for Veracity" by Steve Reeves available at https://arxiv.org/abs/2302.06164.

This work was completed as a part of the Veracity Lab which was one of the Spearhead projects of the Science for Technological Innovation National Science Challenge (SfTI) in New Zealand.

Contents

Imports
Converting rational numbers to strings
Start of the formalisation of the veracity logic
Types for names
Types of aspects of the veracity logic
- Claims
- Evidence
- Actors
- Trust Relations
- Judgements
Helpful extras
The machinery for equality treating lists as sets
The central inductive definition of valid proof trees
- Helper for when only the actor and claim is known up front
String representations
Examples
- Example application of each rule
  - assume
  - bot_elim
  - and_intro
  - and_elim1
  - and_elim2
  - or_intro1
  - or_intro2
  - or_elim1
  - or_elim2
  - trust
  - impl_intro
  - impl_elim
- Other examples
Addional notes

Imports

List, ListNotations, String, Strings.Ascii and Bool are required for various aspects of this formalisation as one might expect. In particular, String and Strings.Ascii are required because a key feature of this formalisation is the ability to output strings as LaTeX, natural language, or formatted for LogSeq.

QArith and QArith.Qminmax are imported because rational numbers are used to represent weights (e.g. how much does one actor trust another). We chose rational numbers rather than real numbers because rational numbers are much easier to work with and the additional expressivity of real numbers is not necessary here.

Require Import List.
Import ListNotations.
Require Import String.
Require Import Strings.Ascii.
Require Import Bool.
Require Import Program.
Require Import QArith.
Require Import QArith.Qminmax.

Converting rational numbers to strings

Coq does not natively include a function to convert rational numbers to strings (or even natural numbers). Here we define a function that prints rational numbers as strings formatted for LaTeX. E.g. as \frac{3}{8} i.e. \(\frac{3}{8}\).

The following writeNat function and those it depends on are used under the MIT License, they are by @arthuraa on GitHub. See: https://github.com/arthuraa/poleiro/blob/master/theories/ReadNat.v

Open Scope char_scope.
Open Scope nat_scope.

Definition natToDigit (n : nat) : ascii :=
  match n with
    | 0 => "0"
    | 1 => "1"
    | 2 => "2"
    | 3 => "3"
    | 4 => "4"
    | 5 => "5"
    | 6 => "6"
    | 7 => "7"
    | 8 => "8"
    | _ => "9"
  end.

Fixpoint writeNatAux (time n : nat) (acc : string) : string :=
  let acc' := String (natToDigit (n mod 10)) acc in
  match time with
    | 0 => acc'
    | S time' =>
      match n / 10 with
        | 0 => acc'
        | n' => writeNatAux time' n' acc'
      end
  end.

Definition writeNat (n : nat) : string :=
  writeNatAux n n "".

Eval compute in writeNat 42.= "42"%string
: string

Close Scope nat_scope.

Eval compute in Qnum 0.5.= 5%Z
: Z
Eval compute in Qden 0.5.= 10%positive
: positive
Eval compute in Qnum (Qred 0.5).= 1%Z
: Z
Eval compute in Qden (Qred 0.5).= 2%positive
: positive

Open Scope nat_scope.
Definition writeQ (x : Q) : string :=
  let simplified := Qred x in
  let numerator := Z.to_nat (Qnum simplified) in
  let denominator := Pos.to_nat (Qden simplified) in
  if (denominator =? 1) then writeNat numerator else
  "\frac{" 
    ++  (writeNat numerator) 
    ++ "}{" 
    ++ (writeNat denominator) ++ "}".
Eval compute in writeQ 0.35.= "\frac{7}{20}"%string
: string

Definition writeQNaturalLanguage (x : Q) : string :=
  let simplified := Qred x in
  let numerator := Z.to_nat (Qnum simplified) in
  let denominator := Pos.to_nat (Qden simplified) in
  if (denominator =? 1) then writeNat numerator else
    (writeNat numerator) 
    ++ "/" 
    ++ (writeNat denominator).
Eval compute in writeQNaturalLanguage 0.35.= "7/20"%string
: string
Close Scope nat_scope.

Eval compute in writeQ 0.35.= "\frac{7}{20}"%string
: string

Start of the formalisation of the veracity logic

With the preliminaries covered, we now begin to introduce the definitions directly related to the veracity logic.

Section VeracityLogic.

Types for names

First, we introduce inductive types for the names of atomic evidence, actors and trust relations.

We use Scheme Equality for ... to automatically generate functions such as atomic_evid_name_beq which are boolean equality functions for each of the inductive types for names.

For more information on Scheme Equality, please see: https://coq.inria.fr/doc/V8.17.1/refman/proofs/writing-proofs/reasoning-inductives.html#coq:cmd.Scheme-Equality.

Inductive atomic_evid_name :=
  | _e_
  | _e1_
  | _e2_
  | _e3_
  | _e4_
  | _eQ_
  | _eB_
  | _l_
  | _s_
  | _c_
  | _x_
  | _y_
  | _z_
  | _belief_
  | _testing_
  | _audit_
  | _compile_
  | _review_
  | _assess_
  | _business_procedure_
  | _ingredients_percentage_list_
  | _breakdown_of_formulations_list_
.

Scheme Equality for atomic_evid_name.
Check atomic_evid_name_beq.atomic_evid_name_beq
     : atomic_evid_name -> atomic_evid_name -> bool

The Check command, above, prints the type of the term following it.

Inductive actor_name :=
  | _a1_
  | _a2_
  | _a3_
  | _a4_
  | _aQ_
  | _retailer_
  | _vineyard_
  | _winery_
  | _P_
  | _Q_
  | _R_
  | _S_
  | _T_
  | _U_
  | _L_
  | _applicant_
  | _certifier_
.

Scheme Equality for actor_name.
Check actor_name_beq.actor_name_beq
     : actor_name -> actor_name -> bool

Inductive claim_name :=
  | _c1_
  | _c2_
  | _c3_
  | _c4_
  | _c5_
  | _cQ_
  | _healthy_
  | _nonToxic_
  | _organic_
  | _ingredients_valid_
  | _ingredients_valid_approved_
  | _recipe_valid_
  | _percentage_ingredients_valid_
  | _breakdown_of_formulations_valid_
  | _successful_market_compliance_assessment_
. 

Scheme Equality for claim_name.
Check claim_name_beq.claim_name_beq
     : claim_name -> claim_name -> bool

Inductive trust_relation_name :=
  | _A_Trust_
  | _B_Trust_
  | _T_Trust_
  | _U_Trust_
  | _V_Trust_
.

Scheme Equality for trust_relation_name.
Check trust_relation_name_beq.trust_relation_name_beq
     : trust_relation_name ->
       trust_relation_name -> bool

Types of aspects of the veracity logic

Claims

First, we have the inductive type for claims. A claim can either be:

A named atomic claim

Bottom, the claim which can never have veracity

A conjuction of two other claims

A disjucntion of two other claims

We again use Scheme Equality to define boolean equality for claims.

Inductive claim :=
  | AtomicClaim (n : claim_name)
  | Bottom
  | And (c1 c2 : claim)
  | Or  (c1 c2 : claim)
  | Implies  (c1 c2 : claim).

Scheme Equality for claim.

Evidence

Secondly, we have the inductive type for evidence. Evidence can either be:

Named atomic evidence

A pair of other evidence (used for claims which are a conjunction)

Evidence tagged with Left (used for claims which are a disjunction where the left disjunct is true)

Evidence tagged with Right (used for claims which are a disjunction where the right disjunct is true)

Evidence that involves an abstraction, described further below (used for implicative claims)

An experimental alternative implementation of evid which uses dependent types to make the links described in the parentheses explicit can be found on the branch WIP-dependent-evid here: https://github.com/Coda-Coda/Veracity-Logic-Mechanised/blob/WIP-dependent-evid/Coq/VeracityLogic.v#L331. The experimental WIP-dependent-evid branch was only completed up to the definition of proofTreeOf and does not include working versions of the example proofs.

We again use Scheme Equality to define boolean equality for evidence.

Abstractions turn out to be challenging to formalise, especially when including weights. The solution taken in this formalisation at the moment is to require evidence of the same weight to be used when a lambda is applied as back when the lambda was constructed. This requires the formalisation to keep track of the weights used when lambdas are constructed, and so Lambda has the argument required_weight.

Inductive evid :=
  | AtomicEvid (n : atomic_evid_name)
  | Pair (e1 e2: evid)
  | Left (e1 : evid)
  | Right (e1 : evid)
  | Lambda (x : atomic_evid_name) (required_weight : Q) (bx : evid).

Scheme Equality for evid.

Actors

Next, we have the inductive type for actors.

An actor can only be:

A tagged actor_name

We again use Scheme Equality to define boolean equality for actors.

Inductive actor :=
  | Actor (n : actor_name).

Scheme Equality for actor.

Trust Relations

Next, we have the inductive type for trust relations.

Similarly to actors, a trust_relation can only be:

A tagged trust_relation_name

We again use Scheme Equality to define boolean equality for trust relations.

Inductive trustRelation :=
  | Trust (n : trust_relation_name).

Scheme Equality for trustRelation.

Judgements

Finally, we have the inductive type for judgements.

A judgement has one constructor which requries:

Evidence, an Actor, a Weight, and a Claim.

This is taken to mean that based on the provided evidence, the given actor holds that the given claim has veracity, at the strength of the given weight.

We again use Scheme Equality to define boolean equality for judgements.

Inductive judgement :=
  Judgement (e : evid) (a : actor) (w : Q) (c: claim).

Scheme Equality for judgement.

The machinery for equality treating lists as sets

We would like to treat assumptions as sets, because the order of assumptions is irrelevant and we would like to not be concerned with duplicate assumptions. The only operation we need to apply to assumptions is equality, which is used in the logical rules in the proofTreeOf definition later. So, here we take the straightforward approach of defining eq_sets which is an equality function treating lists as sets, defined as both lists being a subset of each other.

The notation {Beq A} preceded by a backquote indicates that the type A is of the typeclass Beq described earlier, see Boolean equality typeclass. So, eq_sets defines equality for lists treated as sets containing elements of a type which has a boolean equality function declared for it. The typeclass instance for Beq is what defines =? in the definitions below, as this was the notation we defined for beq. In this file we only use eq_sets for lists of evidence, but for the sake of generality we use the Beq typeclass.

Fixpoint contains {A} `{Beq A} (x : A) (l : list A) : bool :=
  match l with
  | [] => false
  | h :: tl => (x =? h) || contains x tl
  end.

Fixpoint subset {A} `{Beq A} (l1 l2 : list A) : bool :=
  match l1 with
  | [] => true
  | h :: tl => contains h l2 && subset tl l2
end.

Definition eq_sets {A} `{Beq A} (l1 l2 : list A) : bool := subset l1 l2 && subset l2 l1.

We also define the notation ==? for eq_sets.

Infix "==?" := eq_sets (at level 70) : beq_scope.

The central inductive definition of valid proof trees

Now we move to the most important definition of this file. The inductive type proofTreeOf defines what a correct proof tree can be. At it's core, it is a datatype for a tree. However, it is dependently typed, the type depends on the values list judgement (the list/set of assumptions) and judgement (the judgement that this proof tree). That is, proofTreeOf Ps j is the type of all correct proof trees of the judgement j with the assumptions Ps.

In the rules we use the convention of naming variables as follows:

Ps, Qs, Rs refer to the lists/sets of assumptions (we represent assumptions as judgements).

e, e1, e2 refer to evidence or, in some cases, atomic evidence names when we require the evidence to be atomic.

a, a1, a2 refer to actors.

w, w1, w2 refer to weights, of type Q.

c, c1, c2 refer to claims.

H, H1, H2 refer to "hypotheses" or, in these rules, conditions that must be met for the rule/constructor to be able to be applied. They are sometimes followed by a description, e.g. HWeights refers to a condition to do with weights.

In these rules, we rely on Coq's type inference, so we don't explicity give the types of e a w and c in the assume rule, for example. But we could instead have written:

| assume (e : atomic_evid_name) (a : actor) (w : Q) (c : claim) ...

A helpful exercise may be to add explicit types like this whenever the types are not 100% clear and check if Coq still accepts the definition.

It is important to realise that proofTreeOf is a dependent Type (rather than a Prop), so we can pattern match on values of type proofTreeOf Ps j and use this to define functions on proof trees, such as converting them to Latex strings. The alternative would have been to make proofTreeOf an inductive proposition. For more information on inductive propositions see: https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html. Previous/VeracityLogicV1.v and Previous/VeracityLogicV2.v took the inductive proposition approach.

For each rule, everything before the final colon is required in order to construct the proof tree that follows the final colon.

For example, in and_intro, for any:

evidence e1, e2

actor a

weights w1, w2, w3

claims C1, C2

assumptions Ps, Qs, Rs

As well as:

a proof that the assumptions in Rs equals (Ps appended to Qs) (considered as sets)

a proof that w3 is the minimum of w1 and w2

Along with:

a proof tree from the assumptions Ps of the judgement that the actor a holds that C1 has veracity with weight w1 by the evidence e1

and a proof tree from the assumptions Qs of the judgement that the actor a holds that C2 has veracity with weight w2 by the evidence e2

We then have constructed:

a proof tree from the assumptions Rs of the judgement that the actor a holds that \(C_1 \wedge C_2\) has veracity with weight w3 by the evidence \((e_1,e_2)\).

Further details of each rule are discussed later in: Example application of each rule.

Inductive proofTreeOf : list judgement -> judgement -> Type :=
| assume (e : atomic_evid_name) (a : actor) (w : Q) (c : claim) : proofTreeOf [((AtomicEvid e) \by a @ w \in c)] ((AtomicEvid e) \by a @ w \in c)

| bot_elim e a w C Ps

        (M : proofTreeOf Ps (e \by a @ w \in _|_))
                           :
             proofTreeOf Ps (e \by a @ w \in C)

| and_intro e1 e2 a w1 w2 w3 C1 C2 Ps Qs Rs
         (H : Ps ++ Qs ==? Rs = true)
         (HWeights : w3 = Qmin w1 w2)

(L: proofTreeOf Ps (e1 \by a @ w1 \in C1))
                           (R: proofTreeOf Qs (e2 \by a @ w2 \in C2))
                        :
    proofTreeOf Rs ({{e1, e2}} \by a @ w3 \in (C1 /\' C2))

| and_elim1 e1 e2 a w C1 C2 Ps

    (M : proofTreeOf Ps ({{e1, e2}} \by a @ w \in (C1 /\' C2)))
                           :
             proofTreeOf Ps (e1 \by a @ w \in C1)

| and_elim2 e1 e2 a w C1 C2 Ps

    (M : proofTreeOf Ps ({{e1, e2}} \by a @ w \in (C1 /\' C2)))
                          :
        proofTreeOf Ps (e2 \by a @ w \in C2)

| or_intro1 e1 a w C1 C2 Ps

           (M: proofTreeOf Ps (e1 \by a @ w \in C1))
                          :
    proofTreeOf Ps ((Left e1) \by a @ w \in (C1 \/' C2))

| or_intro2 e2 a w C1 C2 Ps

           (M: proofTreeOf Ps (e2 \by a @ w \in C2))
                          :
    proofTreeOf Ps ((Right e2) \by a @ w \in (C1 \/' C2))

| or_elim1 e1 a w C1 C2 Ps

    (M: proofTreeOf Ps ((Left e1) \by a @ w \in (C1 \/' C2)))
                        :
      proofTreeOf Ps (e1 \by a @ w \in C1)

| or_elim2 e2 a w C1 C2 Ps

    (M : proofTreeOf Ps ((Right e2) \by a @ w \in (C1 \/' C2)))
                          :
        proofTreeOf Ps (e2 \by a @ w \in C2)

| trust e a1 a2 wTrust w1 w2 C (name : trustRelation) Ps
                    (HWeights : w2 = w1 * wTrust)

(L: proofTreeOf Ps (e \by a2 @ w1 \in C))
                          :
            proofTreeOf Ps (e \by a1 @ w2 \in C)

| impl_intro (x : atomic_evid_name) (bx : evid) a w1 w2 (C1 : claim) C2 Ps Qs
                    (H1 : notUsedInInnerAbstraction x bx = true)
                 (H2 : contains ((AtomicEvid x) \by a @ w1 \in C1) Ps = true)
                 (H3 : remove judgement_eq_dec ((AtomicEvid x) \by a @ w1 \in C1) Ps ==? Qs = true)

              (M: proofTreeOf Ps (bx \by a @ w2 \in C2))
                              :
   proofTreeOf Qs ((Lambda x w1 bx) \by a @ w2 \in (Implies C1 C2))
| impl_elim x bx y a w1 w2 C1 C2 Ps Qs Rs
                    (H1 : Ps ++ Qs ==? Rs = true)
               (H2 : notUsedInInnerAbstraction x bx = true)                

(L: proofTreeOf Ps ((Lambda x w1 bx) \by a @ w2 \in (Implies C1 C2)))
                           (R: proofTreeOf Qs (y \by a @ w1 \in C1))
                        :
    proofTreeOf Rs ((apply_abstraction x bx y H2) \by a @ w2 \in C2)
.

Helper for when only the actor and claim is known up front

proofTreeOf_wrapped is a dependent record which makes it more convenient to represent the type of a proof tree involving an actor holding that some claim has veracity, but where the evidence and list of assumptions is not known up front. It is a dependent record because the type of _p depends on the values from the earlier fields _Ps, _e and _w.

This allows us to start "proofs" (i.e. proof mode sessions where we are constructing a value of the proofTreeOf type) by only specifiying the actor and claim, using the tactic eexists to let Coq assist in filling out the evidence and list of assumptions.

For more information on Coq's records see: https://coq.inria.fr/doc/V8.17.1/refman/language/core/records.html.

Record proofTreeOf_wrapped (a : actor) (c : claim) := {
  _Ps : list judgement;
  _e : evid;
  _w : Q;
  _p : proofTreeOf _Ps (_e \by a @ _w \in c)
}.

String representations

Here we define the functions which ultimately convert proof trees (values of type proofTreeOf Ps j) into string representations for:

Latex (making use of the bussproofs package)

Natural language (indented plain text)

LogSeq (a text-based note-taking tool supporting collapsable nested bullets, available from https://logseq.com/)

First we define typeclasses for each type of show. Show/show are typically used as the names for the typeclass/function which convert datatypes to a string. For more infomation on typeclasses, see the link in the section Boolean equality typeclass.

Open Scope string.

Class ShowForProofTree A : Type :=
  {
    showForProofTree : A -> string
  }.
Class ShowForNaturalLanguage A : Type :=
  {
    showForNaturalLanguage : A -> string
  }.
Class ShowForLogSeq A : Type :=
  {
    showForLogSeq : A -> string
  }.

For printing rational numbers (for weights) we will use writeQ for Latex and LogSeq (since LogSeq supports basic Latex commands in "math mode"), and writeQNaturalLanguage for natural language. writeQ and writeQNaturalLanguage were defined earlier in Converting rational numbers to strings.

Instance : ShowForProofTree Q := { showForProofTree := writeQ }.
Instance : ShowForNaturalLanguage Q := { showForNaturalLanguage := writeQNaturalLanguage }.
Instance : ShowForLogSeq Q := { showForLogSeq := writeQ }.

Now we can write the following:

Eval compute in showForProofTree 0.125.= "\frac{1}{8}"
: string
Eval compute in showForNaturalLanguage 0.125.= "1/8"
: string

Next, we define the string representations of the names given to atomic evidence, actors, claims and trust relations.

Instance : ShowForProofTree atomic_evid_name := { 
  showForProofTree n := 
    match n with
      | _e_ => "e"
      | _e1_ => "e1"
      | _e2_ => "e2"
      | _e3_ => "e3"
      | _e4_ => "e4"
      | _eQ_ => "e?"
      | _eB_ => "eB"
      | _l_ => "l"
      | _s_ => "s"
      | _c_ => "c"
      | _x_ => "x"
      | _y_ => "y"
      | _z_ => "z"
      | _belief_ => "b"
      | _testing_ => "t"
      | _audit_ => "a"
      | _compile_=> "c"
      | _review_=> "r"
      | _assess_ => "a"
      | _business_procedure_ => "p"
      | _ingredients_percentage_list_ => "ePI"
      | _breakdown_of_formulations_list_=> "eBF"
    end
  }.

Instance : ShowForProofTree actor_name := { 
  showForProofTree n := 
    match n with
      | _a1_ => "a_{1}"
      | _a2_ => "a_{2}"
      | _a3_ => "a_{3}"
      | _a4_ => "a_{4}"
      | _aQ_ => "a_{?}"
      | _retailer_ => "r"
      | _vineyard_ => "v"
      | _winery_ => "w"
      | _P_ => "P"
      | _Q_ => "Q"
      | _R_ => "R"
      | _S_ => "S"
      | _T_ => "T"
      | _U_ => "U"
      | _L_ => "L"
      | _applicant_ => "A"
      | _certifier_ => "C"
    end
  }.

Instance : ShowForProofTree claim_name := { 
  showForProofTree n := 
    match n with
      | _c1_ => "C_{1}"
      | _c2_ => "C_{2}"
      | _c3_ => "C_{3}"
      | _c4_ => "C_{4}"
      | _c5_ => "C_{5}"
      | _cQ_ => "C_{?}"
      | _healthy_ => "H"
      | _nonToxic_ => "N"
      | _organic_ => "O"
      | _ingredients_valid_ => "\mathit{IV}"
      | _ingredients_valid_approved_ => "\mathit{IVA}"
      | _recipe_valid_ => "\mathit{RV}"      
      | _percentage_ingredients_valid_ => "\mathit{PIV}"
      | _breakdown_of_formulations_valid_ => "\mathit{BFV}"
      | _successful_market_compliance_assessment_ => "\mathit{SMCA}"
    end
  }.

Instance : ShowForProofTree trust_relation_name := { 
  showForProofTree n := 
    match n with
      | _A_Trust_ => "A"
      | _B_Trust_ => "B"
      | _T_Trust_ => "T"
      | _U_Trust_ => "U"
      | _V_Trust_ => "V"
    end
  }.

Instance : ShowForNaturalLanguage atomic_evid_name := { 
  showForNaturalLanguage n := 
    match n with
      | _e_ => "atomic evidence e"
      | _e1_ => "atomic evidence 1"
      | _e2_ => "atomic evidence 2"
      | _e3_ => "atomic evidence 3"
      | _e4_ => "atomic evidence 4"
      | _eQ_ =>  "unknown evidence"
      | _eB_ =>  "evidence for bottom"
      | _l_ => "atomic evidence l"
      | _s_ => "atomic evidence s"
      | _c_ => "atomic evidence c"
      | _x_ => "atomic evidence x"
      | _y_ => "atomic evidence y"
      | _z_ => "atomic evidence z"
      | _belief_ => "belief"
      | _testing_ => "testing"
      | _audit_ => "audit"
      | _compile_=> "compile"
      | _review_=> "review"
      | _assess_ => "assess"
      | _business_procedure_ => "business procedure"
      | _ingredients_percentage_list_ => "ingredients percentage list"
      | _breakdown_of_formulations_list_ => "breakdown of formulations list"
    end
  }.
Instance : ShowForLogSeq atomic_evid_name := {showForLogSeq := showForNaturalLanguage}.

Instance : ShowForNaturalLanguage actor_name := { 
  showForNaturalLanguage n := 
    match n with
      | _a1_ => "actor 1"
      | _a2_ => "actor 2"
      | _a3_ => "actor 3"
      | _a4_ => "actor 4"
      | _aQ_ => "unknown actor"
      | _retailer_ => "retailer"
      | _vineyard_ => "vineyard"
      | _winery_ => "winery"
      | _P_ => "Penelope"
      | _Q_ => "Quentin"
      | _R_ => "Ryan"
      | _S_ => "Samantha"
      | _T_ => "Tom"
      | _U_ => "Ulysses"
      | _L_ => "Ledger"
      | _applicant_ => "applicant"
      | _certifier_ => "certifier"
    end
  }.
Instance : ShowForLogSeq actor_name := {showForLogSeq := showForNaturalLanguage}.

Instance : ShowForNaturalLanguage claim_name := { 
  showForNaturalLanguage n := 
    match n with
      | _c1_ => "claim 1"
      | _c2_ => "claim 2"
      | _c3_ => "claim 3"
      | _c4_ => "claim 4"
      | _c5_ => "claim 5"
      | _cQ_ => "unknown claim"
      | _healthy_ => "healthy"
      | _nonToxic_ => "non-toxic"
      | _organic_ => "organic"
      | _ingredients_valid_ => "ingredients-valid"
      | _ingredients_valid_approved_ => "ingredients-valid-approved"
      | _recipe_valid_ => "recipe-valid"      
      | _percentage_ingredients_valid_ => "percentage-ingredients-valid"
      | _breakdown_of_formulations_valid_ => "breakdown-of-formulations-valid"
      | _successful_market_compliance_assessment_ => "successful-market-compliance-assessment"
    end
  }.
Instance : ShowForLogSeq claim_name := {showForLogSeq := showForNaturalLanguage}.

Instance : ShowForNaturalLanguage trust_relation_name := { 
  showForNaturalLanguage n := 
    match n with
      | _A_Trust_ => "trust relation A"
      | _B_Trust_ => "trust relation B"
      | _T_Trust_ => "trust relation T"
      | _U_Trust_ => "trust relation U"
      | _V_Trust_ => "trust relation V"
    end
  }.
Instance : ShowForLogSeq trust_relation_name := {showForLogSeq := showForNaturalLanguage}.

Now we define how to represent evidence, using a recursive functions.

Fixpoint showForProofTreeEvid e :=
  match e with
  | AtomicEvid name => showForProofTree name
  | Pair e1 e2 => "(" ++ (showForProofTreeEvid e1) ++ ", "
                      ++ (showForProofTreeEvid e2) ++ ")"
  | Left e => "i(" ++ showForProofTreeEvid e ++ ")"
  | Right e => "j(" ++ showForProofTreeEvid e ++ ")"
  | Lambda e1 w e2 => "\lambda(" ++ showForProofTree e1 ++ "_{" ++ showForProofTree w ++ "})(" ++ showForProofTreeEvid e2 ++ ")"
end.

For now, all three representations print evidence the same way. This is not ideal for the natural language representation, which could be improved in the future.

Instance : ShowForProofTree evid := { showForProofTree := showForProofTreeEvid }.
Instance : ShowForNaturalLanguage evid := { showForNaturalLanguage := showForProofTree }.
Instance : ShowForLogSeq evid := {showForLogSeq := showForNaturalLanguage}.

Here are a couple of examples of printing evidence:

Eval compute in showForProofTree {{e1, Left e2}}.= "(e1, i(e2))"
: string
Eval compute in showForProofTree (Lambda _e1_ (1#2) (Right e1)).= "\lambda(e1_{\frac{1}{2}})(j(e1))"
: string

Here we define the representation of claims. For the sake of brevity, we use fix to inline the recursive function.

For more information on fix and Fixpoint see: https://coq.inria.fr/doc/V8.17.1/refman/language/core/inductive.html?highlight=fix#recursive-functions-fix and https://coq.inria.fr/doc/V8.17.1/refman/language/core/inductive.html?highlight=fix#top-level-recursive-functions.

Instance : ShowForProofTree claim := {
  showForProofTree :=
  fix showForProofTreeClaim c :=
    match c with
      | AtomicClaim name => showForProofTree name
      | Bottom => "\bot"
      | And c1 c2 => "(" ++ showForProofTreeClaim c1 ++ " \wedge " ++ showForProofTreeClaim c2 ++ ")"
      | Or c1 c2 => "(" ++ showForProofTreeClaim c1 ++ " \vee " ++ showForProofTreeClaim c2 ++ ")"
      | Implies c1 c2 => "(" ++ showForProofTreeClaim c1 ++ " \rightarrow " ++ showForProofTreeClaim c2 ++ ")"
    end
}.

Instance : ShowForNaturalLanguage claim := {
  showForNaturalLanguage :=
  fix showForNaturalLanguageClaim c :=
    match c with
      | AtomicClaim name => showForNaturalLanguage name
      | Bottom => "impossible"
      | And c1 c2 => "(" ++ showForNaturalLanguageClaim c1 ++ " and " ++ showForNaturalLanguageClaim c2  ++ ")"
      | Or c1 c2 => "(" ++ showForNaturalLanguageClaim c1 ++ " or " ++ showForNaturalLanguageClaim c2 ++ ")"
      | Implies c1 c2 => "(" ++ showForNaturalLanguageClaim c1 ++ " implies " ++ showForNaturalLanguageClaim c2 ++ ")"
    end
}.
Instance : ShowForLogSeq claim := {showForLogSeq := showForNaturalLanguage}.

Here are a couple of examples of printing claims:

Eval compute in showForProofTree (c1 \/' c2).= "(C_{1} \vee C_{2})"
: string
Eval compute in showForLogSeq (c1 \/' c2).= "(claim 1 or claim 2)"
: string

Eval compute in showForProofTree ((c1 /\' c2) ->' c2).= "((C_{1} \wedge C_{2}) \rightarrow C_{2})"
: string
Eval compute in showForLogSeq ((c1 /\' c2) ->' c2).= "((claim 1 and claim 2) implies claim 2)"
: string

Here we define how to print the tagged types actor and trustRelation by simply printing the names as defined earlier.

Instance : ShowForProofTree actor := {
  showForProofTree a :=
  match a with
    | Actor name => showForProofTree name
  end
}.

Instance : ShowForNaturalLanguage actor := {
  showForNaturalLanguage a :=
  match a with
    | Actor name => showForNaturalLanguage name
  end
}.

Instance : ShowForLogSeq actor := {
  showForLogSeq a :=
  match a with
    | Actor name => showForLogSeq name
  end
}.

Instance : ShowForProofTree trustRelation := {
  showForProofTree t :=
  match t with
    | Trust name => showForProofTree name
  end
}.

Instance : ShowForNaturalLanguage trustRelation := {
  showForNaturalLanguage t :=
  match t with
    | Trust name => showForNaturalLanguage name
  end
}.

Instance : ShowForLogSeq trustRelation := {
  showForLogSeq t :=
  match t with
    | Trust name => showForLogSeq name
  end
}.

We will need to be able to print lists in certain scenarios (e.g. lists of assumptions or of trust relations that were used). The way we would like to print these lists differs for Latex, natural language and LogSeq.

The notation of {ShowForProofTree A} preceded by a backtick indicates that the type A must be of the typeclass ShowForProofTree. So, these functions are defined for printing lists which contain a type for which ShowForProofTree has been defined (or whichever of ShowForNaturalLanguage or ShowForLogSeq is indicated).

Fixpoint showForProofTree_list {A} `{ShowForProofTree A} (l : list A) :=
  match l with
    | [] => ""
    | [h] => showForProofTree h
    | h1 :: (h2 :: tl) as tl' => showForProofTree h1 ++ ", " ++ showForProofTree_list tl'
  end.

Instance showForProofTree_list_instance (A : Type) `(ShowForProofTree A) : ShowForProofTree (list A) := {
  showForProofTree l := showForProofTree_list l
}.

Fixpoint showForNaturalLanguage_list {A} `{ShowForNaturalLanguage A} (l : list A) :=
  match l with
    | [] => "no items"
    | [h] => showForNaturalLanguage h
    | [h1;h2] => showForNaturalLanguage h1 ++ ", and " ++ showForNaturalLanguage h2
    | h1 :: (h2 :: tl) as tl' => showForNaturalLanguage h1 ++ ", " ++ showForNaturalLanguage_list tl'
  end.Unused variable tl might be a misspelled constructor.
Use _ or _tl to silence this warning.
[unused-pattern-matching-variable,pattern-matching]
Instance showForNaturalLanguage_list_instance (A : Type) `(ShowForNaturalLanguage A) : ShowForNaturalLanguage (list A) := {
    showForNaturalLanguage l := showForNaturalLanguage_list l
  }.

We don't create a typeclass instance of showForLogSeq for lists because we need to pass an additional parameter indent to produces strings that are appropriately indented for the LogSeq output.

Fixpoint showForLogSeq_list {A} `{ShowForLogSeq A} (indent : string) (l : list A) :=
  match l with
    | [] => ""
    | [h] => indent ++ "- " ++ showForLogSeq h
    | h :: tl => indent ++ "- " ++ showForLogSeq h ++ "
" ++ showForLogSeq_list indent tl
  end.

Here are few examples of printing lists.

Eval compute in showForProofTree [].= ""
: string
Eval compute in showForProofTree [(Left e2)].= "i(e2)"
: string
Eval compute in showForProofTree [(Left e2);e1].= "i(e2), e1"
: string

Eval compute in showForNaturalLanguage [].= "no items"
: string
Eval compute in showForNaturalLanguage [(Left e2)].= "i(e2)"
: string
Eval compute in showForNaturalLanguage [(Left e2);e1].= "i(e2), and e1"
: string

Eval compute in showForLogSeq_list "  " [].= ""
: string
Eval compute in showForLogSeq_list "  " [(Left e2)].= "  - i(e2)"
: string
Eval compute in showForLogSeq_list "  " [(Left e2);e1].   = "  - i(e2)
- e1"
   : string

Here we define how to show judgements. This relies on the previous definitions for printing evidence, actors, weights and claims.

Instance : ShowForProofTree judgement := {
  showForProofTree j :=
  match j with
  | Judgement e a w c => showForProofTree e ++ "^{" ++ showForProofTree a ++ "}_{" 
                         ++ showForProofTree w ++ "} \in " ++ showForProofTree c
  end
}.

Instance : ShowForNaturalLanguage judgement := {
  showForNaturalLanguage j :=
  match j with
  | Judgement e a w c => showForNaturalLanguage c ++ " is supported by $" ++ showForNaturalLanguage e ++ "$ at weight " ++ showForNaturalLanguage w ++ " which " ++ showForNaturalLanguage a ++ " uses"
  end
}.

Instance : ShowForLogSeq judgement := {
  showForLogSeq j :=
  match j with
  | Judgement e a w c => showForLogSeq c ++ " is held by " ++ showForLogSeq a ++ " by the evidence $" ++ showForLogSeq e ++ "$ at weight $" ++ showForLogSeq w ++ "$"
  end
}.

Here are a few examples of printing the type judgement.

Eval compute in showForProofTree (x \by Penelope @ 1 \in c1).= "x^{P}_{1} \in C_{1}"
: string
Eval compute in showForNaturalLanguage (x \by Penelope @ 1 \in c1).= "claim 1 is supported by $x$ at weight 1 which Penelope uses"
: string
Eval compute in showForLogSeq (x \by Penelope @ 1 \in c1).= "claim 1 is held by Penelope by the evidence $x$ at weight $1$"
: string

The name "judgement" is also used to refer to a judgement along with its assumptions and the trust relations used in its proof. Here we define how to print this generalised form. We also pass as an argument to these functions the argument (p : proofTreeOf Ps j) which is the proof of the judgement. The definitions here don't directly make use of p, however when calling them we will typically have a proof tree p in our context and so instead of writing the arguments Ps and j explicitly we can then use Coq's type inference to compute them.

Definition showForProofTree_judgement (Ts : list trustRelation) (Ps : list judgement) (j : judgement) (p : proofTreeOf Ps j) :=
    match Ps with
      | [] => showForProofTree j
      | (h :: tl) as Ps => showForProofTree Ps ++ " \vdash_{" ++ showForProofTree Ts ++ "} " ++ (showForProofTree j)
    end.

Definition showForNaturalLanguage_judgement (Ts : list trustRelation) (Ps : list judgement) (j : judgement) (p : proofTreeOf Ps j) :=
  match Ps with
    | [] => showForNaturalLanguage j
    | (h :: tl) as Ps => "Assuming " ++ showForNaturalLanguage Ps ++ " then " ++ showForNaturalLanguage j
  end.

Definition showForLogSeq_judgement (Ts : list trustRelation) (indent : string) (Ps : list judgement) (j : judgement) (p : proofTreeOf Ps j) :=
  match Ps,Ts with
        | [],[] => showForLogSeq j
        | (h :: tl),[] => showForLogSeq j ++ "
" ++ indent ++ "collapsed:: true
" ++ indent ++ "- " ++ "Assumptions made:
" ++ indent ++ "  collapsed:: true
" ++ showForLogSeq_list ("  " ++ indent) Ps
        | [],(h :: tl) => showForLogSeq j ++ "
" ++ indent ++ "collapsed:: true
" ++ indent ++ "- " ++ "Trust relations used:
" ++ indent ++ "  collapsed:: true
" ++ showForLogSeq_list ("  " ++ indent) Ts
        | (h :: tl),(h2::tl2) => showForLogSeq j ++ "
" ++ indent ++ "collapsed:: true
" ++ indent ++ "- " ++ "Assumptions made:
" ++ indent ++ "  collapsed:: true
" ++ showForLogSeq_list ("  " ++ indent) Ps ++ "
" ++ indent ++ "- " ++ "Trust relations used:
" ++ indent ++ "  collapsed:: true
" ++ showForLogSeq_list ("  " ++ indent) Ts
  end.

Here are a few examples of printing the generalised form of judgements:

Eval compute in showForProofTree_judgement [trustT;trustU] [x \by Quentin @ 1 \in c1] (x \by Penelope @ 1 \in c1) _.= "x^{Q}_{1} \in C_{1} \vdash_{T, U} x^{P}_{1} \in C_{1}"
: string
Eval compute in showForNaturalLanguage_judgement [trustT;trustU] [x \by Quentin @ 1 \in c1] (x \by Penelope @ 1 \in c1) _.= "Assuming claim 1 is supported by $x$ at weight 1 which Quentin uses then claim 1 is supported by $x$ at weight 1 which Penelope uses"
: string
Eval compute in showForLogSeq_judgement [trustT;trustU] "" [x \by Quentin @ 1 \in c1] (x \by Penelope @ 1 \in c1) _.     = "claim 1 is held by Penelope by the evidence $x$ at weight $1$
collapsed:: true
- Assumptions made:
  collapsed:: true
  - claim 1 is held by Quentin by the evidence $x$ at weight $1$
- Trust relations used:
  collapsed:: true
  - trust relation T
  - trust relation U"
     : string

Eval compute in showForProofTree_judgement [] [(e1 \by a1 @ 1 \in c1)] (e1 \by a1 @ 1 \in c1) (assume _e1_ a1 1 c1).= "e1^{a_{1}}_{1} \in C_{1} \vdash_{} e1^{a_{1}}_{1} \in C_{1}"
: string
Eval compute in showForNaturalLanguage_judgement [] [(e1 \by a1 @ 1 \in c1)] (e1 \by a1 @ 1 \in c1) (assume _e1_ a1 1 c1).= "Assuming claim 1 is supported by $e1$ at weight 1 which actor 1 uses then claim 1 is supported by $e1$ at weight 1 which actor 1 uses"
: string
Eval compute in showForLogSeq_judgement [] "" [(e1 \by a1 @ 1 \in c1)] (e1 \by a1 @ 1 \in c1) (assume _e1_ a1 1 c1).     = "claim 1 is held by actor 1 by the evidence $e1$ at weight $1$
collapsed:: true
- Assumptions made:
  collapsed:: true
  - claim 1 is held by actor 1 by the evidence $e1$ at weight $1$"
     : string

We need to compute which trust relations were used during the proofs, so that we can print them.

Fixpoint getAllTrustRelationsUsed (Ps : list judgement) (j : judgement) (p : proofTreeOf Ps j)
  : list trustRelation :=
match p with
| assume e a w C => []
| bot_elim e a w C Ps M => getAllTrustRelationsUsed _ _ M
| and_intro e1 e2 a w1 w2 w3 C1 C2 Ps Qs Rs H HWeight L R => 
    getAllTrustRelationsUsed _ _ L ++ getAllTrustRelationsUsed _ _ R 
| and_elim1 e1 e2 a w C1 C2 Ps M => getAllTrustRelationsUsed _ _ M
| and_elim2 e1 e2 a w C1 C2 Ps M => getAllTrustRelationsUsed _ _ M
| or_intro1 e1 a w C1 C2 Ps M => getAllTrustRelationsUsed _ _ M
| or_intro2 e2 a w C1 C2 Ps M => getAllTrustRelationsUsed _ _ M
| or_elim1 e1 a w C1 C2 Ps M => getAllTrustRelationsUsed _ _ M
| or_elim2 e2 a w C1 C2 Ps M => getAllTrustRelationsUsed _ _ M
| trust e a1 a2 wTrust w1 w2 C name Ps HWeight L => name :: getAllTrustRelationsUsed _ _ L
| impl_intro _ _ _ _ _ _ _ _ _ _ _ _ M => getAllTrustRelationsUsed _ _ M
| impl_elim _ _ _ _ _ _ _ _ _ _ _ _ _ L R => getAllTrustRelationsUsed _ _ L ++ getAllTrustRelationsUsed _ _ R 
end.

In the LogSeq output, we print out a bulleted list of what longer names correspond to the shorter names for evidence. So, we need to compute a list of all the evidence that was used in the proof, to construct this summary of the evidence names.

Fixpoint getAllEvidence (Ps : list judgement) (j : judgement) (p : proofTreeOf Ps j)
  : list evid :=
match p with
| assume e a w C => [(AtomicEvid e)]
| bot_elim e a w C _ M => (getAllEvidence _ _ M)
| and_intro e1 e2 a w1 w2 w3 C1 C2 Ps Qs Rs H HWeight L R => getAllEvidence _ _ L ++ getAllEvidence _ _ R 
| and_elim1 e1 e2 a w C1 C2 _ M => getAllEvidence _ _ M
| and_elim2 e1 e2 a w C1 C2 _ M => getAllEvidence _ _ M
| or_intro1 e1 a w C1 C2 _ M => getAllEvidence _ _ M
| or_intro2 e2 a w C1 C2 _ M => getAllEvidence _ _ M
| or_elim1 e1 a w C1 C2 _ M => getAllEvidence _ _ M
| or_elim2 e2 a w C1 C2 _ M => getAllEvidence _ _ M
| trust e a1 a2 wTrust w1 w2 C name _ _ L => getAllEvidence _ _ L
| impl_intro _ _ _ _ _ _ _ _ _ _ _ _ M => getAllEvidence _ _ M
| impl_elim _ _ _ _ _ _ _ _ _ _ _ _ _ _ M => getAllEvidence _ _ M
end.

We also will need a helper function to filter out non-atomic evidence from the summary of evidence names.

Definition isAtomicEvidence (e : evid) : bool :=
match e with
  | AtomicEvid _ => true
  | _ => false
end.

In some scenarios, we will wish to remove duplicates from lists that are being treated as sets before we print them. removeDups removes duplicates from lists which hold a type which is of the Beq typeclass.

Fixpoint removeDups {A} `{Beq A} (l : list A) : list A :=
    match l with
    | [] => []
    | h :: tl => if existsb (beq h) tl then removeDups tl else h :: removeDups tl
    end.

We now define the representation of proof trees, which is the main purpose of this section. These helper functions provide the core functionality related to printing proof trees.

For showForProofTree we make use of bussproofs commands. For more information on bussproofs, see https://ctan.org/pkg/bussproofs. We assume that the Latex file already includes: \usepackage{bussproofs}. The commands used are also compatible with MathJax for incorporating into webpages. For more information on MathJax see: https://www.mathjax.org/. Mathjax's functionality is used to make Alectryon's html output render the proof trees.

As an aside, this file is written in a literate programming style intended to be processed by the tool Alectryon. Alectryon, as used here, generates HTML which includes the output from running the Coq commands in this file, showing some outputs explictly due to command such as .unfold. For more information about Alectryon see: https://github.com/cpitclaudel/alectryon. It is used under the MIT license.

To install Alectryon, this repository uses the Nix Package Manager (https://nixos.org), however Alectryon can be installed using other methods such as using opam as described here: https://github.com/cpitclaudel/alectryon?tab=readme-ov-file#setup. If you have Nix installed (see: https://nixos.org/download/), simply running nix-shell from the Coq subdirectory will install Alectryon and Coq v8.17 as specified in the shell.nix file in the Coq subdirectory.

The command:

cd Coq; nix-shell --run "time alectryon --long-line-threshold 999999 --output-directory html VeracityLogic.v"

Will build Coq/html/VeracityLogic.html after installing the dependencies (if not yet installed). (When run from the root of this repository).

tasks.json sets up VSCode to carry this out upon Ctrl+Shift+B.

The files in .devcontainer set up Nix and build VeracityLogic.html when opened as a GitHub Codespace (all that is needed is a browser!). See the README for more information.

As mentioned before the aside, here are the core definitions defining the string representations of proof trees.

Fixpoint showForProofTree_proofTreeOf_helper (Ps : list judgement) (j : judgement) (p : proofTreeOf Ps j)
  : string :=
let Ts := (removeDups (getAllTrustRelationsUsed Ps j p)) in
match p with
| assume e a w C => "\AxiomC{$ " 
             ++ showForProofTree C 
             ++ " \textit{ is a veracity claim} $}"
    ++ " \RightLabel{ $ assume $}\UnaryInfC{$ "
    ++ showForProofTree_judgement Ts _ _ p ++ " $}"
| bot_elim e a w C _ M => showForProofTree_proofTreeOf_helper _ _ M
    ++ " \RightLabel{ $ \bot^{-} $} \UnaryInfC{$ "
    ++ showForProofTree_judgement Ts _ _ p
    ++ " $}"
| and_intro e1 e2 a w1 w2 w3 C1 C2 _ _ _ _ _ L R => 
    showForProofTree_proofTreeOf_helper _ _ L
 ++ showForProofTree_proofTreeOf_helper _ _ R 
 ++ " \RightLabel{ $ \wedge^{+} $} \BinaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p ++ " $}"
| and_elim1 e1 e2 a w C1 C2 _ M => showForProofTree_proofTreeOf_helper _ _ M
 ++ " \RightLabel{ $ \land^{-1} $} \UnaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p
 ++ " $}"
| and_elim2 e1 e2 a w C1 C2 _ M => showForProofTree_proofTreeOf_helper _ _ M
 ++ " \RightLabel{ $ \land^{-2} $} \UnaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p
 ++ " $}"
| or_intro1 e1 a w C1 C2 _ M => showForProofTree_proofTreeOf_helper _ _ M
 ++ " \RightLabel{ $ \lor^{+1} $} \UnaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p
 ++ " $}"
| or_intro2 e2 a w C1 C2_ _ M => showForProofTree_proofTreeOf_helper _ _ M
 ++ " \RightLabel{ $ \lor^{+2} $} \UnaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p
 ++ " $}"
| or_elim1 e1 a w C1 C2_ _ M => showForProofTree_proofTreeOf_helper _ _ M
 ++ " \RightLabel{ $ \lor^{-1} $} \UnaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p
 ++ " $}"
| or_elim2 e2 a w C1 C2 _ M => showForProofTree_proofTreeOf_helper _ _ M
 ++ " \RightLabel{ $ \lor^{-2} $} \UnaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p
 ++ " $}"
| trust e a1 a2 wTrust w1 w2 C name _ _ L => 
    showForProofTree_proofTreeOf_helper _ _ L
 ++ " \AxiomC{$" ++ showForProofTree a1 ++ showForProofTree name ++ showForProofTree a2 ++ "$} "
 ++ " \RightLabel{ $ trust\ " ++ showForProofTree name ++ "\ (" ++ showForProofTree wTrust ++ ")"
 ++ "$} \BinaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p ++ " $}"
| impl_intro e1 e2 a w1 w2 C1 C2 H _ _ _ _ M => showForProofTree_proofTreeOf_helper _ _ M
 ++ " \RightLabel{ $ \rightarrow^+ $} \UnaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p
 ++ " $}"
| impl_elim x bx y a w1 w2 C1 C2 H1 _ _ _ _ L R => 
     showForProofTree_proofTreeOf_helper _ _ L
 ++ showForProofTree_proofTreeOf_helper _ _ R 
 ++ " \RightLabel{ $ \rightarrow^{-} $} \BinaryInfC{$ "
 ++ showForProofTree_judgement Ts _ _ p ++ " $}"
end.

Fixpoint showForNaturalLanguage_proofTreeOf_helper (indent : string) (Ps : list judgement) (j : judgement) (p : proofTreeOf Ps j)
  : string :=
let Ts := (removeDups (getAllTrustRelationsUsed Ps j p)) in
match p with
| assume e a w C => 
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ "  " ++ indent ++ showForNaturalLanguage C ++ " is a veracity claim." ++ "
"
++ indent ++ "by assumption."
| bot_elim e a w C _ M =>
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ M ++ "
"
++ indent ++ "by the logical principle of explosion."
| and_intro e1 e2 a w1 w2 w3 C1 C2 _ _ _ _ _ L R => 
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ L ++ "
"
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ R ++ "
"
++ indent ++ "by a logical rule for 'and'."
| and_elim1 e1 e2 a w C1 C2 _ M =>
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ M ++ "
"
++ indent ++ "by a logical rule for 'and'."
| and_elim2 e1 e2 a w C1 C2 _ M => 
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ M ++ "
"
++ indent ++ "by a logical rule for 'and'."
| or_intro1 e1 a w C1 C2 _ M =>
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ M ++ "
"
++ indent ++ "by a logical rule for 'or'."
| or_intro2 e2 a w C1 C2 _ M =>
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ M ++ "
"
++ indent ++ "by a logical rule for 'or'."
| or_elim1 e1 a w C1 C2 _ M =>
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ M ++ "
"
++ indent ++ "by a logical rule for 'or'."
| or_elim2 e2 a w C1 C2 _ M => 
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ M ++ "
"
++ indent ++ "by a logical rule for 'or'."
| trust e a1 a2 wTrust w1 w2 C name _ _ L => 
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ L ++ "
"
++ indent ++ "by the trust relation " ++ showForNaturalLanguage name ++ " with weight " ++ showForNaturalLanguage wTrust ++ "."
| impl_intro _ _ _ _ _ _ _ _ _ _ _ _ M => 
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ M ++ "
"
++ indent ++ "by a logical rule for implication."
| impl_elim _ _ _ _ _ _  _ _ _ _ _ _ _ L R => 
indent ++ showForNaturalLanguage_judgement Ts _ _ p ++ ", because
" 
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ L ++ "
"
++ showForNaturalLanguage_proofTreeOf_helper ("  " ++ indent) _ _ R ++ "
"
++ indent ++ "by a logical rule for implication."
end.

Fixpoint showForLogSeq_proofTreeOf_helper (indent : string) (Ps : list judgement) (j : judgement) (p : proofTreeOf Ps j)
  : string :=
let Ts := (removeDups (getAllTrustRelationsUsed Ps j p)) in
match p with
| assume e a w C => 
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: we assume this"
| bot_elim e a w C _ M =>
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: the principle of explosion
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ M
| and_intro e1 e2 a w1 w2 w3 C1 C2 _ _ _ _ _ L R => 
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: and introduction
    " ++ indent ++ "- " ++ "Sub-proofs:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ L ++ "
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ R
| and_elim1 e1 e2 a w C1 C2 _ M =>
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: and elimination (1)
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ M
| and_elim2 e1 e2 a w C1 C2 _ M => 
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: and elimination (2)
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ M
| or_intro1 e1 a w C1 C2 _ M =>
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: or introduction (1)
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ M
| or_intro2 e2 a w C1 C2 _ M =>
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: or introduction (2)
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ M
| or_elim1 e1 a w C1 C2 _ M =>
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: or elimination (1)
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ M
| or_elim2 e2 a w C1 C2 _ M => 
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: or elimination (2)
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ M
| trust e a1 a2 wTrust w1 w2 C name _ _ L => 
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: trust, with relation " ++ showForLogSeq name ++ " with weight $" ++ showForLogSeq wTrust ++ "$
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ L
| impl_intro _ _ _ _ _ _ _ _ _ _ _ _ M => 
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: implication introduction
    " ++ indent ++ "- " ++ "Sub-proof:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ M
| impl_elim _ _ _ _ _ _  _ _ _ _ _ _ _ L R => 
indent ++ "- " ++ showForLogSeq_judgement Ts ("  " ++ indent) _ _ p ++ "
  " ++ indent ++ "- " ++ "Logical rule used: implication elimination
    " ++ indent ++ "- " ++ "Sub-proofs:
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ L ++ "
" ++ showForLogSeq_proofTreeOf_helper ("      " ++ indent) _ _ R
end.

Next are some helper functions which make it possible to print lists of proof trees and which wrap the string output of proof trees with a title or Latex begin/end command as appropriate.

Open Scope string.

Fixpoint showForProofTree_list_newline {A} `{ShowForProofTree A} (l : list A) :=
  match l with
    | [] => ""
    | [h] => showForProofTree h
    | h1 :: (h2 :: tl) as tl' => showForProofTree h1 ++ "
" ++ showForProofTree_list_newline tl'
  end.

Definition showForProofTree_proofTreeOf Ps j p
  := "\begin{prooftree}" ++ showForProofTree_proofTreeOf_helper Ps j p
       ++ "\end{prooftree}".
Instance showForProofTree_proofTreeOf_instance Ps (j : judgement)
  : ShowForProofTree (proofTreeOf Ps j) := { showForProofTree := showForProofTree_proofTreeOf Ps j}.

Definition showForNaturalLanguage_proofTreeOf Ps j (p : proofTreeOf Ps j) := "

" ++ showForNaturalLanguage_proofTreeOf_helper "- " Ps j p ++ "

".
Instance showForNaturalLanguage_proofTreeOf_instance Ps (j : judgement)
  : ShowForNaturalLanguage (proofTreeOf Ps j) := { showForNaturalLanguage := showForNaturalLanguage_proofTreeOf Ps j}.

Definition printProofTitle j :=
match j with
| Judgement e a w c => "### Veracity proof that " ++ showForLogSeq c ++ " is held by " ++ showForLogSeq a ++ " by the evidence $" ++ showForLogSeq e ++ "$ at weight $" ++ showForLogSeq w ++ "$"
end.

Instance : ShowForLogSeq string := { showForLogSeq := id}.

Definition showForLogSeq_proofTreeOf Ps j (p : proofTreeOf Ps j) := 
let evidenceList := (removeDups (filter isAtomicEvidence (getAllEvidence Ps j p))) in
let evidenceWithNames := map (fun e => match e with
                                   | AtomicEvid n => showForLogSeq e ++ " = " ++ showForLogSeq n
                                   | _ => ""
                                   end) evidenceList in
"

" ++ printProofTitle j ++ "
" ++ showForLogSeq_proofTreeOf_helper "  " Ps j p ++ "
  - Atomic evidence is abbreviated as follows:
    collapsed:: true
" ++ showForLogSeq_list "    " evidenceWithNames ++ "

".
Instance showForLogSeq_proofTreeOf_instance Ps (j : judgement)
  : ShowForLogSeq (proofTreeOf Ps j) := { showForLogSeq := showForLogSeq_proofTreeOf Ps j}.

Fixpoint showListOfProofTrees {Ps} {j : judgement} (l : list (proofTreeOf Ps j)) :=
    match l with
      | [] => ""
      | h :: tl => "

----------------

" ++ showForProofTree h ++ showListOfProofTrees tl
    end.

Here we define how to print the proofTreeOf_wrapped type, which helps when we don't know the evidence or assumptions up front. We simply extract the _p value from the record, which is of type proofTreeOf Ps j, and then print it as defined above.

Instance showForProofTree_proofTreeOf_wrapped_instance (a : actor) (c : claim) : ShowForProofTree (proofTreeOf_wrapped a c) := { showForProofTree p := showForProofTree (_p a c p) }.
Instance showForNaturalLanguage_proofTreeOf_wrapped_instance (a : actor) (c : claim) : ShowForNaturalLanguage (proofTreeOf_wrapped a c) := { showForNaturalLanguage p := showForNaturalLanguage (_p a c p) }.
Instance showForLogSeq_proofTreeOf_wrapped_instance (a : actor) (c : claim) : ShowForLogSeq (proofTreeOf_wrapped a c) := { showForLogSeq p := showForLogSeq (_p a c p) }.

Open Scope beq_scope.

For examples of proof trees being printed, please see the outputs in the Examples section, next.

Addional notes

The proof trees on this page are rendered using MathJax which happens to require at least one explicit math command. Hence: \(x\) is included here so that the proof tree rendering continues to work even if all other comments including math commands are removed.

When viewing this file directly as a .v file, the syntax:

.. coq:: unfold
  :class: coq-math

Indicates the beginning of a Coq snippet that should be unfolded with the output rendered using MathJax's Latex. This is used for rendering proof trees.

These snippets are followed by:

.. coq::

To indicate that the default should now be to leave Coq commands folded and not to render the output using MathJax. The class coq-math is a CSS class, which interacts with the code following:

.. raw:: html

Which is near the start of this file, in order to load and render MathJax when appropriate.

Finally, some CSS overrides are defined in Coq/html/overrides.css which improve the look of the output.