prev slide prev contents next next slide

Encoding CIC in XML: an example of exported object


The principle of induction over natural numbers in Coq:

  Coq < Print nat_ind.
  nat_ind = 
  [P:(nat->Prop); f:(P O); f0:((n:nat)(P n)->(P (S n)))]
   Fix F
     {F [n:nat] : (P n) :=
        Cases n of
          O => f
        | (S n0) => (f0 n0 (F n0))
        end}
       : (P:(nat->Prop))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)
 

The corresponding XML file:

  <?xml version="1.0" encoding="ISO-8859-1"?>
  <!DOCTYPE Definition SYSTEM "http://localhost:8081/getdtd?url=cic.dtd">

  <Definition name="nat_ind" params="">
    <body>
      <LAMBDA>
        <source>
          <PROD>
            <source>
              <MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
            </source>
            <target>
              <SORT value="Prop"/>
            </target>
          </PROD>
        </source>
        <target binder="P">
          <LAMBDA>
            <source>
              <APPLY>
                <REL value="1" binder="P"/>
                <MUTCONSTRUCT uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0" noConstr="1"/>
              </APPLY>
            </source>
            <target binder="f">
              <LAMBDA>
                <source>
                  <PROD>
                    <source>
                      <MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
                    </source>
                    <target binder="n">
                      <PROD>
                        <source>
                          <APPLY>
                            <REL value="3" binder="P"/>
                            <REL value="1" binder="n"/>
                          </APPLY>
                        </source>
                        <target>
                          <APPLY>
                            <REL value="4" binder="P"/>
                            <APPLY>
                              <MUTCONSTRUCT uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0" noConstr="2"/>
                              <REL value="2" binder="n"/>
                            </APPLY>
                          </APPLY>
                        </target>
                      </PROD>
                    </target>
                  </PROD>
                </source>
                <target binder="f0">
                  <FIX noFun="0">
                    <FixFunction name="F" recIndex="0">
                      <type>
                        <PROD>
                          <source>
                            <MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
                          </source>
                          <target binder="n">
                            <APPLY>
                              <REL value="4" binder="P"/>
                              <REL value="1" binder="n"/>
                            </APPLY>
                          </target>
                        </PROD>
                      </type>
                      <body>
                        <LAMBDA>
                          <source>
                            <MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
                          </source>
                          <target binder="n">
                            <MUTCASE uriType="cic:/coq/INIT/Datatypes/nat.ind" noType="0">
                              <patternsType>
                                <REL value="5" binder="P"/>
                              </patternsType>
                              <inductiveTerm>
                                <REL value="1" binder="n"/>
                              </inductiveTerm>
                              <pattern>
                                <REL value="4" binder="f"/>
                              </pattern>
                              <pattern>
                                <LAMBDA>
                                  <source>
                                    <MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
                                  </source>
                                  <target binder="n0">
                                    <APPLY>
                                      <REL value="4" binder="f0"/>
                                      <REL value="1" binder="n0"/>
                                      <APPLY>
                                        <REL value="3" binder="F"/>
                                        <REL value="1" binder="n0"/>
                                      </APPLY>
                                    </APPLY>
                                  </target>
                                </LAMBDA>
                              </pattern>
                            </MUTCASE>
                          </target>
                        </LAMBDA>
                      </body>
                    </FixFunction>
                  </FIX>
                </target>
              </LAMBDA>
            </target>
          </LAMBDA>
        </target>
      </LAMBDA>
    </body>
    <type>
      <CAST>
        <term>
          <PROD>
            <source>
              <PROD>
                <source>
                  <MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
                </source>
                <target>
                  <SORT value="Prop"/>
                </target>
              </PROD>
            </source>
            <target binder="P">
              <PROD>
                <source>
                  <APPLY>
                    <REL value="1" binder="P"/>
                    <MUTCONSTRUCT uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0" noConstr="1"/>
                  </APPLY>
                </source>
                <target binder="f">
                  <PROD>
                    <source>
                      <PROD>
                        <source>
                          <MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
                        </source>
                        <target binder="n">
                          <PROD>
                            <source>
                              <APPLY>
                                <REL value="3" binder="P"/>
                                <REL value="1" binder="n"/>
                              </APPLY>
                            </source>
                            <target>
                              <APPLY>
                                <REL value="4" binder="P"/>
                                <APPLY>
                                  <MUTCONSTRUCT uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0" noConstr="2"/>
                                  <REL value="2" binder="n"/>
                                </APPLY>
                              </APPLY>
                            </target>
                          </PROD>
                        </target>
                      </PROD>
                    </source>
                    <target binder="f0">
                      <PROD>
                        <source>
                          <MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
                        </source>
                        <target binder="n">
                          <APPLY>
                            <REL value="4" binder="P"/>
                            <REL value="1" binder="n"/>
                          </APPLY>
                        </target>
                      </PROD>
                    </target>
                  </PROD>
                </target>
              </PROD>
            </target>
          </PROD>
        </term>
        <type>
          <SORT value="Prop"/>
        </type>
      </CAST>
    </type>
  </Definition>