Usage of ProofDocFormat
Usage of ProofDocFormat
In[]:=
<<"EosHeader.m"
Command ProofDocFormat is used to format the cell groups in Program Section of the generated proofDoc.
1. Introduction
1. Introduction
Suppose we want to structure the following program cells in Program Section of the proofDoc generated by executing the program cells (see the next section Program).
In[]:=
EosSession["Example of use of ProofDocFormat"];
In[]:=
MarkOn[];
In[]:=
NewOrigami[10];
In[]:=
HO["A","B"]!
In[]:=
NewPoint[{"G"{5,7}}]
In[]:=
HO["A","C"]!
In[]:=
map={"A"{0,0},"B"{1,0},"C"{1,1},"D"{0,1},"G"{u,v}};
In[]:=
Goal[IncidentQ["G","EF"]SquaredDistance["G","A"]==SquaredDistanc.e["G","B"]∧SquaredDistance["G","C"]==SquaredDistance["G","D"]];
In[]:=
EndSession[]
We need to insert proofDoc formatting commands at the points where you want subsection grouping. The following is what we would like to.
In[]:=
EosSession["Example of use of ProofDocFormat"];
In[]:=
MarkOn[];
In[]:=
ProofDocFormat["Construction","Subsection","Keep"];
In[]:=
NewOrigami[10];
In[]:=
HO["A","B"]!
In[]:=
NewPoint[{"G"{5,7}}]
In[]:=
HO["A","C"]!
In[]:=
ProofDocFormat["Proof","Subsection",1,"Remove"];
ProofDocFormat["Goal","Subsubsection","Remove"];
In[]:=
map={"A"{0,0},"B"{1,0},"C"{1,1},"D"{0,1},"G"{u,v}};
In[]:=
Goal[IncidentQ["G","EF"]SquaredDistance["G","A"]==SquaredDistanc.e["G","B"]∧SquaredDistance["G","C"]==SquaredDistance["G","D"]];
In[]:=
ProofDocFormat["Prove","Subsubsection","Keep"];
In[]:=
Prove["Example",Mappingmap]
In[]:=
EndSession[];
2. Function of ProofDocFormat
2. Function of ProofDocFormat
In the above, the pink cells are inserted.
The format of ProofDocFormat is
ProofDoc[title, section, keep] or ProofDoc[title, section, open, keep] where
section is a string of either “subsection” or “subsubsection”, and
title is a string that exoress the title of the section,
open is 1, which means the section is closed, and
keep is either “Keep” or “Remove”, specifying this format command is kept in the output or removed.
ProofDoc[title, section, keep] or ProofDoc[title, section, open, keep] where
section is a string of either “subsection” or “subsubsection”, and
title is a string that exoress the title of the section,
open is 1, which means the section is closed, and
keep is either “Keep” or “Remove”, specifying this format command is kept in the output or removed.
We can also specify
ProofDoc[title, section]
ProofDoc[title, section]
This means ProofDoc[title, section,1,”Remove”]
3. The result
3. The result
TheresultooftheexecutionoftheOrikotoprograminSection1isthefollowing:
Program
Program
EosSession["Example of use of ProofDocFormat"];
MarkOn[];
Construction
Construction
ProofDocFormat["Construction","Subsection","Keep"];
NewOrigami[10];
HO["A","B"]!
NewPoint[{"G"{5,7}}]
HO["A","C"]!
Proof
Proof
4. Exercise: Try the following and see the Program Section of the output proofDoc.
4. Exercise: Try the following and see the Program Section of the output proofDoc.
In[]:=
EosSession["Example of use of ProofDocFormat"];
In[]:=
MarkOn[];
Construction
Construction
In[]:=
ProofDocFormat["Construction","Subsection"];
In[]:=
NewOrigami[10];
In[]:=
HO["A","B"]!
In[]:=
NewPoint[{"G"{5,7}}]
In[]:=
HO["A","C"]!
Proof
Proof
In[]:=
ProofDocFormat["Proof","Subsection"];
In[]:=
ProofDocFormat["Goal","Subsubsection"];
In[]:=
map={"A"{0,0},"B"{1,0},"C"{1,1},"D"{0,1},"G"{u,v}};
In[]:=
Goal[IncidentQ["G","EF"]SquaredDistance["G","A"]==SquaredDistanc.e["G","B"]∧SquaredDistance["G","C"]==SquaredDistance["G","D"]];
In[]:=
ProofDocFormat["Prove","Subsubsection",1(*,"Remove"*)];
In[]:=
Prove["Exercise",Mappingmap]
EndSession[];