Linguist 2.1.0

Closes #207

README.md

@@ -8,7 +8,9 @@ We use this library at GitHub to detect blob languages, highlight code, ignore b
 
 Linguist defines the list of all languages known to GitHub in a [yaml file](https://github.com/github/linguist/blob/master/lib/linguist/languages.yml). In order for a file to be highlighted, a language and lexer must be defined there.
 
-Most languages are detected by their file extension. This is the fastest and most common situation. For script files, which are usually extensionless, we do "deep content inspection"™ and check the shebang of the file. Checking the file's contents may also be used for disambiguating languages. C, C++ and Obj-C all use `.h` files. Looking for common keywords, we are usually able to guess the correct language.
+Most languages are detected by their file extension. This is the fastest and most common situation.
+
+For disambiguating between files with common extensions, we use a [bayesian classifier](https://github.com/github/linguist/blob/master/lib/linguist/classifier.rb). For an example, this helps us tell the difference between `.h` files which could be either C, C++, or Obj-C.
 
 In the actual GitHub app we deal with `Grit::Blob` objects. For testing, there is a simple `FileBlob` API.
 
@@ -22,23 +24,11 @@ See [lib/linguist/language.rb](https://github.com/github/linguist/blob/master/li
 
 The actual syntax highlighting is handled by our Pygments wrapper, [pygments.rb](https://github.com/tmm1/pygments.rb). It also provides a [Lexer abstraction](https://github.com/tmm1/pygments.rb/blob/master/lib/pygments/lexer.rb) that determines which highlighter should be used on a file.
 
-We typically run on a prerelease version of Pygments to get early access to new lexers. The [lexers.yml](https://github.com/github/linguist/blob/master/lib/linguist/lexers.yml) file is a dump of the lexers we have available on our server. If there is a new lexer in pygments-main not on the list, [open an issue](https://github.com/github/linguist/issues) and we'll try to upgrade it soon.
-
-### MIME type detection
-
-Most of the MIME types handling is done by the Ruby [mime-types gem](https://github.com/halostatue/mime-types). But we have our own list of additions and overrides. To add or modify this list, see [lib/linguist/mimes.yml](https://github.com/github/linguist/blob/master/lib/linguist/mimes.yml).
-
-MIME types are used to set the Content-Type of raw binary blobs which are served from a special `raw.github.com` domain. However, all text blobs are served as `text/plain` regardless of their type to ensure they open in the browser rather than downloading.
-
-The MIME type also determines whether a blob is binary or plain text. So if you're seeing a blob that says "View Raw" and it is actually plain text, the mime type and encoding probably needs to be explicitly stated.
-
-    Linguist::FileBlob.new("linguist.zip").binary? #=> true
-
-See [lib/linguist/mimes.yml](https://github.com/github/linguist/blob/master/lib/linguist/mimes.yml).
+We typically run on a prerelease version of Pygments, [pygments.rb](https://github.com/tmm1/pygments.rb), to get early access to new lexers. The [lexers.yml](https://github.com/github/linguist/blob/master/lib/linguist/lexers.yml) file is a dump of the lexers we have available on our server.
 
 ### Stats
 
-The [Language Graph](https://github.com/github/linguist/graphs/languages) is built by aggregating the languages of all repo's blobs. The top language in the graph determines the project's primary language. Collectively, these stats make up the [Top Languages](https://github.com/languages) page.
+The Language Graph you see on every repository is built by aggregating the languages of all repo's blobs. The top language in the graph determines the project's primary language. Collectively, these stats make up the [Top Languages](https://github.com/languages) page.
 
 The repository stats API can be used on a directory:
 
@@ -70,7 +60,9 @@ See [Linguist::BlobHelper#generated?](https://github.com/github/linguist/blob/ma
 
 ## Installation
 
-To get it, clone the repo and run [Bundler](http://gembundler.com/) to install its dependencies.
+github.com is usually running the latest version of the `github-linguist` gem that is released on [RubyGems.org](http://rubygems.org/gems/github-linguist).
+
+But for development you are going to want to checkout out the source. To get it, clone the repo and run [Bundler](http://gembundler.com/) to install its dependencies.
 
     git clone https://github.com/github/linguist.git
     cd linguist/
@@ -80,17 +72,14 @@ To run the tests:
 
     bundle exec rake test
 
-*Since this code is specific to GitHub, is not published as a official rubygem.*
-
-If you are seeing errors like `StandardError: could not find any magic files!`, it means the CharlockHolmes gem didn’t install correctly. See the [installing section](https://github.com/brianmario/charlock_holmes/blob/master/README.md) of the CharlockHolmes README for more information.
-
 ## Contributing
 
-1. Fork it.
-2. Create a branch (`git checkout -b detect-foo-language`)
-3. Make your changes
-4. Run the tests (`bundle install` then `bundle exec rake`)
-5. Commit your changes (`git commit -am "Added detection for the new Foo language"`)
-6. Push to the branch (`git push origin detect-foo-language`)
-7. Create a [Pull Request](http://help.github.com/pull-requests/) from your branch.
-8. Promote it. Get others to drop in and +1 it.
+The majority of patches won't need to touch any Ruby code at all. The [master language list](https://github.com/github/linguist/blob/master/lib/linguist/languages.yml) is just a configuration file.
+
+Almost all bug fixes or new language additions should come with some additional code samples. Just drop them under [`samples/`](https://github.com/github/linguist/tree/master/samples) in the correct subdirectory and our test suite will automatically test them. In most cases you shouldn't need to add any new assertions.
+
+### Testing
+
+Sometimes getting the tests running can be to much work especially if you don't have much Ruby experience. Its okay, be lazy and let our build bot [Travis](http://travis-ci.org/#!/github/linguist) run the tests for you. Just open a pull request and the bot will start cranking away.
+
+Heres our current build status, which is hopefully green: [![Build Status](https://secure.travis-ci.org/github/linguist.png?branch=master)](http://travis-ci.org/github/linguist)

Rakefile

@@ -7,23 +7,21 @@ Rake::TestTask.new do |t|
   t.warning = true
 end
 
-
-file 'lib/linguist/classifier.yml' => Dir['test/fixtures/**/*'] do |f|
-  require 'linguist/sample'
-  classifier = Linguist::Sample.classifier
-  File.open(f.name, 'w') { |io| YAML.dump(classifier, io) }
+task :samples do
+  require 'linguist/samples'
+  require 'yajl'
+  data = Linguist::Samples.data
+  json = Yajl::Encoder.encode(data, :pretty => true)
+  File.open('lib/linguist/samples.json', 'w') { |io| io.write json }
 end
 
-CLOBBER.include 'lib/linguist/classifier.yml'
-
-task :classifier => ['lib/linguist/classifier.yml']
-
 namespace :classifier do
   LIMIT = 1_000
 
   desc "Run classifier against #{LIMIT} public gists"
   task :test do
     require 'linguist/classifier'
+    require 'linguist/samples'
 
     total, correct, incorrect = 0, 0, 0
     $stdout.sync = true
@@ -32,10 +30,10 @@ namespace :classifier do
       next if file_language.nil? || file_language == 'Text'
       begin
         data = open(file_url).read
-        guessed_language, score = Linguist::Classifier.instance.classify(data).first
+        guessed_language, score = Linguist::Classifier.classify(Linguist::Samples::DATA, data).first
 
         total += 1
-        guessed_language.name == file_language ? correct += 1 : incorrect += 1
+        guessed_language == file_language ? correct += 1 : incorrect += 1
 
         print "\r\e[0K%d:%d  %g%%" % [correct, incorrect, (correct.to_f/total.to_f)*100]
         $stdout.flush

bin/linguist

@@ -28,7 +28,7 @@ elsif File.file?(path)
   puts "  language:  #{blob.language}"
 
   if blob.large?
-    puts "  blob is to large to be shown"
+    puts "  blob is too large to be shown"
   end
 
   if blob.generated?

github-linguist.gemspec

@@ -1,6 +1,6 @@
 Gem::Specification.new do |s|
   s.name    = 'github-linguist'
-  s.version = '2.0.1'
+  s.version = '2.1.0'
   s.summary = "GitHub Language detection"
 
   s.authors = "GitHub"
@@ -14,4 +14,5 @@ Gem::Specification.new do |s|
   s.add_dependency 'pygments.rb',     '~> 0.2.13'
   s.add_development_dependency 'json'
   s.add_development_dependency 'rake'
+  s.add_development_dependency 'yajl-ruby'
 end

lib/linguist.rb

@@ -1,5 +1,5 @@
 require 'linguist/blob_helper'
 require 'linguist/language'
 require 'linguist/mime'
-require 'linguist/pathname'
 require 'linguist/repository'
+require 'linguist/samples'

lib/linguist/blob_helper.rb

@@ -1,7 +1,7 @@
 require 'linguist/classifier'
 require 'linguist/language'
 require 'linguist/mime'
-require 'linguist/pathname'
+require 'linguist/samples'
 
 require 'charlock_holmes'
 require 'escape_utils'
@@ -12,13 +12,6 @@ module Linguist
   # BlobHelper is a mixin for Blobish classes that respond to "name",
   # "data" and "size" such as Grit::Blob.
   module BlobHelper
-    # Internal: Get a Pathname wrapper for Blob#name
-    #
-    # Returns a Pathname.
-    def pathname
-      Pathname.new(name || "")
-    end
-
     # Public: Get the extname of the path
     #
     # Examples
@@ -28,7 +21,7 @@ module Linguist
     #
     # Returns a String
     def extname
-      pathname.extname
+      File.extname(name)
     end
 
     # Public: Get the actual blob mime type
@@ -40,7 +33,7 @@ module Linguist
     #
     # Returns a mime type String.
     def mime_type
-      @mime_type ||= pathname.mime_type
+      @mime_type ||= Mime.mime_for(extname)
     end
 
     # Public: Get the Content-Type header value
@@ -72,7 +65,7 @@ module Linguist
       elsif name.nil?
         "attachment"
       else
-        "attachment; filename=#{EscapeUtils.escape_url(pathname.basename)}"
+        "attachment; filename=#{EscapeUtils.escape_url(File.basename(name))}"
       end
     end
 
@@ -95,7 +88,7 @@ module Linguist
     #
     # Return true or false
     def binary_mime_type?
-      if mime_type = Mime.lookup_mime_type_for(pathname.extname)
+      if mime_type = Mime.lookup_mime_type_for(extname)
         mime_type.binary?
       end
     end
@@ -136,13 +129,6 @@ module Linguist
       ['.png', '.jpg', '.jpeg', '.gif'].include?(extname)
     end
 
-    # Public: Is the blob a possible drupal php file?
-    #
-    # Return true or false
-    def drupal_extname?
-      ['.module', '.install', '.test', '.inc'].include?(extname)
-    end
-
     # Public: Is the blob likely to have a shebang?
     #
     # Return true or false
@@ -428,10 +414,7 @@ module Linguist
       disambiguate_extension_language ||
 
         # See if there is a Language for the extension
-        pathname.language ||
-
-        # Look for idioms in first line
-        first_line_language ||
+        Language.find_by_filename(name) ||
 
         # Try to detect Language from shebang line
         shebang_language
@@ -446,179 +429,18 @@ module Linguist
 
     # Internal: Disambiguates between multiple language extensions.
     #
-    # Delegates to "guess_EXTENSION_language".
-    #
-    # Please add additional test coverage to
-    # `test/test_blob.rb#test_language` if you add another method.
-    #
     # Returns a Language or nil.
     def disambiguate_extension_language
       if Language.ambiguous?(extname)
-        # name = "guess_#{extname.sub(/^\./, '')}_language"
-        # send(name) if respond_to?(name)
-
-        possible_languages = Language.all.select { |l| l.extensions.include?(extname) }
+        possible_languages = Language.all.select { |l| l.extensions.include?(extname) }.map(&:name)
         if possible_languages.any?
-          if result = Classifier.instance.classify(data, possible_languages).first
-            result[0]
+          if result = Classifier.classify(Samples::DATA, data, possible_languages).first
+            Language[result[0]]
           end
         end
       end
     end
 
-    # Internal: Guess language of .cls files
-    #
-    # Returns a Language.
-    def guess_cls_language
-      if lines.grep(/^(%|\\)/).any?
-        Language['TeX']
-      elsif lines.grep(/^\s*(CLASS|METHOD|INTERFACE).*:\s*/i).any? || lines.grep(/^\s*(USING|DEFINE)/i).any?
-        Language['OpenEdge ABL']
-      elsif lines.grep(/\{$/).any? || lines.grep(/\}$/).any?
-        Language['Apex']
-      elsif lines.grep(/^(\'\*|Attribute|Option|Sub|Private|Protected|Public|Friend)/i).any?
-        Language['Visual Basic']
-      else
-        # The most common language should be the fallback
-        Language['TeX']
-      end
-    end
-
-    # Internal: Guess language of header files (.h).
-    #
-    # Returns a Language.
-    def guess_h_language
-      if lines.grep(/^@(interface|property|private|public|end)/).any?
-        Language['Objective-C']
-      elsif lines.grep(/^class |^\s+(public|protected|private):/).any?
-        Language['C++']
-      else
-        Language['C']
-      end
-    end
-
-    # Internal: Guess language of .m files.
-    #
-    # Objective-C heuristics:
-    # * Keywords  ("#import", "#include", "#ifdef", #define, "@end") or "//" and opening "\*" comments
-    #
-    # Matlab heuristics:
-    # * Leading "function " of "classdef " keyword
-    # * "%" comments
-    #
-    # Note: All "#" keywords, e.g., "#import", are guaranteed to be Objective-C. Because the ampersand
-    # is used to created function handles and anonymous functions in Matlab, most "@" keywords are not
-    # safe heuristics. However, "end" is a reserved term in Matlab and can't be used to create a valid
-    # function handle. Because @end is required to close any @implementation, @property, @interface,
-    # @synthesize, etc. directive in Objective-C, only @end needs to be checked for.
-    #
-    # Returns a Language.
-    def guess_m_language
-      # Objective-C keywords or comments
-      if lines.grep(/^#(import|include|ifdef|define)|@end/).any? || lines.grep(/^\s*\/\//).any? || lines.grep(/^\s*\/\*/).any?
-        Language['Objective-C']
-
-      # Matlab file function or class or comments
-      elsif lines.any? && lines.first.match(/^\s*(function |classdef )/) || lines.grep(/^\s*%/).any?
-        Language['Matlab']
-
-      # Fallback to Objective-C, don't want any Matlab false positives
-      else
-        Language['Objective-C']
-      end
-    end
-
-    # Internal: Guess language of .pl files
-    #
-    # The rules for disambiguation are:
-    #
-    # 1. Many perl files begin with a shebang
-    # 2. Most Prolog source files have a rule somewhere (marked by the :- operator)
-    # 3. Default to Perl, because it is more popular
-    #
-    # Returns a Language.
-    def guess_pl_language
-      if shebang_script == 'perl'
-        Language['Perl']
-      elsif lines.grep(/:-/).any?
-        Language['Prolog']
-      else
-        Language['Perl']
-      end
-    end
-
-    # Internal: Guess language of .r files.
-    #
-    # Returns a Language.
-    def guess_r_language
-      if lines.grep(/(rebol|(:\s+func|make\s+object!|^\s*context)\s*\[)/i).any?
-        Language['Rebol']
-      else
-        Language['R']
-      end
-    end
-
-    # Internal: Guess language of .t files.
-    #
-    # Returns a Language.
-    def guess_t_language
-      score = 0
-      score += 1 if lines.grep(/^% /).any?
-      score += data.gsub(/ := /).count
-      score += data.gsub(/proc |procedure |fcn |function /).count
-      score += data.gsub(/var \w+: \w+/).count
-
-      # Tell-tale signs its gotta be Perl
-      if lines.grep(/^(my )?(sub |\$|@|%)\w+/).any?
-        score = 0
-      end
-
-      if score >= 3
-        Language['Turing']
-      else
-        Language['Perl']
-      end
-    end
-
-    # Internal: Guess language of .v files.
-    #
-    # Returns a Language
-    def guess_v_language
-      if lines.grep(/^(\/\*|\/\/|module|parameter|input|output|wire|reg|always|initial|begin|\`)/).any?
-        Language['Verilog']
-      else
-        Language['Coq']
-      end
-    end
-
-    # Internal: Guess language of .gsp files.
-    #
-    # Returns a Language.
-    def guess_gsp_language
-      if lines.grep(/<%|<%@|\$\{|<%|<g:|<meta name="layout"|<r:/).any?
-        Language['Groovy Server Pages']
-      else
-        Language['Gosu']
-      end
-    end
-
-    # Internal: Guess language from the first line.
-    #
-    # Look for leading "<?php" in Drupal files
-    #
-    # Returns a Language.
-    def first_line_language
-      # Only check files with drupal php extensions
-      return unless drupal_extname?
-
-      # Fail fast if blob isn't viewable?
-      return unless viewable?
-
-      if lines.first.to_s =~ /^<\?php/
-        Language['PHP']
-      end
-    end
-
     # Internal: Extract the script name from the shebang line
     #
     # Requires Blob#data
@@ -710,12 +532,5 @@ module Linguist
         ''
       end
     end
-
-    Language.overridden_extensions.each do |extension|
-      name = "guess_#{extension.sub(/^\./, '')}_language".to_sym
-      unless instance_methods.map(&:to_sym).include?(name)
-        raise NotImplementedError, "Language##{name} was not defined"
-      end
-    end
   end
 end

lib/linguist/classifier.rb

@@ -1,113 +1,88 @@
-require 'linguist/language'
 require 'linguist/tokenizer'
 
 module Linguist
   # Language bayesian classifier.
   class Classifier
-    # Internal: Path to persisted classifier db.
-    PATH = File.expand_path('../classifier.yml', __FILE__)
-
-    # Public: Check if persisted db exists on disk.
-    #
-    # Returns Boolean.
-    def self.exist?
-      File.exist?(PATH)
-    end
-
-    # Public: Get persisted Classifier instance.
-    #
-    # Returns Classifier.
-    def self.instance
-      @instance ||= YAML.load_file(PATH)
-    end
-
-    # Public: Initialize a Classifier.
-    def initialize
-      @tokens_total    = 0
-      @languages_total = 0
-      @tokens          = Hash.new { |h, k| h[k] = Hash.new(0) }
-      @language_tokens = Hash.new(0)
-      @languages       = Hash.new(0)
-    end
-
-    # Public: Compare Classifier objects.
-    #
-    # other - Classifier object to compare to.
-    #
-    # Returns Boolean.
-    def eql?(other)
-      # Lazy fast check counts only
-      other.is_a?(self.class) &&
-        @tokens_total == other.instance_variable_get(:@tokens_total) &&
-        @languages_total == other.instance_variable_get(:@languages_total)
-    end
-    alias_method :==, :eql?
-
     # Public: Train classifier that data is a certain language.
     #
-    # language - Language of data
+    # db       - Hash classifier database object
+    # language - String language of data
     # data     - String contents of file
     #
     # Examples
     #
-    #   train(Language['Ruby'], "def hello; end")
+    #   Classifier.train(db, 'Ruby', "def hello; end")
     #
     # Returns nothing.
-    def train(language, data)
-      language = language.name
-      tokens   = Tokenizer.new(data).tokens
+    def self.train!(db, language, data)
+      tokens = Tokenizer.tokenize(data)
+
+      db['tokens_total'] ||= 0
+      db['languages_total'] ||= 0
+      db['tokens'] ||= {}
+      db['language_tokens'] ||= {}
+      db['languages'] ||= {}
 
       tokens.each do |token|
-        @tokens[language][token] += 1
-        @language_tokens[language] += 1
-        @tokens_total += 1
+        db['tokens'][language] ||= {}
+        db['tokens'][language][token] ||= 0
+        db['tokens'][language][token] += 1
+        db['language_tokens'][language] ||= 0
+        db['language_tokens'][language] += 1
+        db['tokens_total'] += 1
       end
-      @languages[language] += 1
-      @languages_total += 1
+      db['languages'][language] ||= 0
+      db['languages'][language] += 1
+      db['languages_total'] += 1
 
       nil
     end
 
-    # Public: Verify internal counts are consistent.
-    #
-    # Returns Boolean.
-    def verify
-      @languages.inject(0) { |n, (l, c)| n += c } == @languages_total &&
-        @language_tokens.inject(0) { |n, (l, c)| n += c } == @tokens_total &&
-        @tokens.inject(0) { |n, (l, ts)| n += ts.inject(0) { |m, (t, c)| m += c } } == @tokens_total
-    end
-
-    # Public: Prune infrequent tokens.
-    #
-    # Returns receiver Classifier instance.
-    def gc
-      self
-    end
-
     # Public: Guess language of data.
     #
+    # db        - Hash of classifer tokens database.
     # data      - Array of tokens or String data to analyze.
-    # languages - Array of Languages to restrict to.
+    # languages - Array of language name Strings to restrict to.
     #
     # Examples
     #
-    #   classify("def hello; end")
-    #   # => [ [Language['Ruby'], 0.90], [Language['Python'], 0.2], ... ]
+    #   Classifier.classify(db, "def hello; end")
+    #   # => [ 'Ruby', 0.90], ['Python', 0.2], ... ]
     #
     # Returns sorted Array of result pairs. Each pair contains the
-    # Language and a Float score.
-    def classify(tokens, languages = @languages.keys)
+    # String language name and a Float score.
+    def self.classify(db, tokens, languages = nil)
+      languages ||= db['languages'].keys
+      new(db).classify(tokens, languages)
+    end
+
+    # Internal: Initialize a Classifier.
+    def initialize(db = {})
+      @tokens_total    = db['tokens_total']
+      @languages_total = db['languages_total']
+      @tokens          = db['tokens']
+      @language_tokens = db['language_tokens']
+      @languages       = db['languages']
+    end
+
+    # Internal: Guess language of data
+    #
+    # data      - Array of tokens or String data to analyze.
+    # languages - Array of language name Strings to restrict to.
+    #
+    # Returns sorted Array of result pairs. Each pair contains the
+    # String language name and a Float score.
+    def classify(tokens, languages)
       return [] if tokens.nil?
-      tokens = Tokenizer.new(tokens).tokens if tokens.is_a?(String)
+      tokens = Tokenizer.tokenize(tokens) if tokens.is_a?(String)
 
       scores = {}
       languages.each do |language|
-        language_name = language.is_a?(Language) ? language.name : language
-        scores[language_name] = tokens_probability(tokens, language_name) +
-                                   language_probability(language_name)
+        scores[language] = tokens_probability(tokens, language) +
+                                   language_probability(language)
       end
 
-      scores.sort { |a, b| b[1] <=> a[1] }.map { |score| [Language[score[0]], score[1]] }
+      scores.sort { |a, b| b[1] <=> a[1] }.map { |score| [score[0], score[1]] }
     end
 
     # Internal: Probably of set of tokens in a language occuring - P(D | C)
@@ -144,41 +119,5 @@ module Linguist
     def language_probability(language)
       Math.log(@languages[language].to_f / @languages_total.to_f)
     end
-
-    # Public: Serialize classifier to YAML.
-    #
-    # opts - Hash of YAML options.
-    #
-    # Returns nothing.
-    def to_yaml(io)
-      data = "--- !ruby/object:Linguist::Classifier\n"
-
-      data << "languages_total: #{@languages_total}\n"
-      data << "tokens_total: #{@tokens_total}\n"
-
-      data << "languages:\n"
-      @languages.sort.each do |language, count|
-        data << "  #{{language => count}.to_yaml.lines.to_a[1]}"
-      end
-
-      data << "language_tokens:\n"
-      @language_tokens.sort.each do |language, count|
-        data << "  #{{language => count}.to_yaml.lines.to_a[1]}"
-      end
-
-      data << "tokens:\n"
-      @tokens.sort.each do |language, tokens|
-        data << "  #{{language => true}.to_yaml.lines.to_a[1].sub(/ true/, "")}"
-        tokens.sort.each do |token, count|
-          data << "    #{{token => count}.to_yaml.lines.to_a[1]}"
-        end
-      end
-
-      io.write data
-      nil
-    end
   end
-
-  # Eager load instance
-  Classifier.instance if Classifier.exist?
 end

lib/linguist/language.rb

@@ -2,6 +2,8 @@ require 'escape_utils'
 require 'pygments'
 require 'yaml'
 
+require 'linguist/samples'
+
 module Linguist
   # Language names that are recognizable by GitHub. Defined languages
   # can be highlighted, searched and listed under the Top Languages page.
@@ -26,13 +28,6 @@ module Linguist
       @overrides.include?(extension)
     end
 
-    # Internal: Return overridden extensions.
-    #
-    # Returns extensions Array.
-    def self.overridden_extensions
-      @overrides.keys
-    end
-
     # Internal: Create a new Language object
     #
     # attributes - A hash of attributes
@@ -244,7 +239,9 @@ module Linguist
       @overrides  = attributes[:overrides]  || []
       @filenames  = attributes[:filenames]  || []
 
-      @primary_extension = attributes[:primary_extension] || default_primary_extension || extensions.first
+      unless @primary_extension = attributes[:primary_extension]
+        raise ArgumentError, "#{@name} is missing primary extension"
+      end
 
       # Prepend primary extension unless its already included
       if primary_extension && !extensions.include?(primary_extension)
@@ -381,13 +378,6 @@ module Linguist
       name.downcase.gsub(/\s/, '-')
     end
 
-    # Internal: Get default primary extension.
-    #
-    # Returns the extension String.
-    def default_primary_extension
-      extensions.first
-    end
-
     # Public: Get Language group
     #
     # Returns a Language
@@ -451,9 +441,34 @@ module Linguist
     end
   end
 
+  extensions = Samples::DATA['extnames']
+  filenames = Samples::DATA['filenames']
   popular = YAML.load_file(File.expand_path("../popular.yml", __FILE__))
 
   YAML.load_file(File.expand_path("../languages.yml", __FILE__)).each do |name, options|
+    options['extensions'] ||= []
+    options['filenames'] ||= []
+
+    if extnames = extensions[name]
+      extnames.each do |extname|
+        if !options['extensions'].include?(extname)
+          options['extensions'] << extname
+        else
+          warn "#{name} #{extname.inspect} is already defined in samples/. Remove from languages.yml."
+        end
+      end
+    end
+
+    if fns = filenames[name]
+      fns.each do |filename|
+        if !options['filenames'].include?(filename)
+          options['filenames'] << filename
+        else
+          warn "#{name} #{filename.inspect} is already defined in samples/. Remove from languages.yml."
+        end
+      end
+    end
+
     Language.create(
       :name              => name,
       :color             => options['color'],
@@ -464,7 +479,7 @@ module Linguist
       :group_name        => options['group'],
       :searchable        => options.key?('searchable') ? options['searchable'] : true,
       :search_term       => options['search_term'],
-      :extensions        => options['extensions'],
+      :extensions        => options['extensions'].sort,
       :primary_extension => options['primary_extension'],
       :overrides         => options['overrides'],
       :filenames         => options['filenames'],

lib/linguist/md5.rb

@@ -0,0 +1,38 @@
+require 'digest/md5'
+
+module Linguist
+  module MD5
+    # Public: Create deep nested digest of value object.
+    #
+    # Useful for object comparsion.
+    #
+    # obj - Object to digest.
+    #
+    # Returns String hex digest
+    def self.hexdigest(obj)
+      digest = Digest::MD5.new
+
+      case obj
+      when String, Symbol, Integer
+        digest.update "#{obj.class}"
+        digest.update "#{obj}"
+      when TrueClass, FalseClass, NilClass
+        digest.update "#{obj.class}"
+      when Array
+        digest.update "#{obj.class}"
+        for e in obj
+          digest.update(hexdigest(e))
+        end
+      when Hash
+        digest.update "#{obj.class}"
+        for e in obj.map { |(k, v)| hexdigest([k, v]) }.sort
+          digest.update(e)
+        end
+      else
+        raise TypeError, "can't convert #{obj.inspect} into String"
+      end
+
+      digest.hexdigest
+    end
+  end
+end

lib/linguist/pathname.rb

@@ -1,92 +0,0 @@
-require 'linguist/language'
-require 'linguist/mime'
-require 'pygments'
-
-module Linguist
-  # Similar to ::Pathname, Linguist::Pathname wraps a path string and
-  # provides helpful query methods. Its useful when you only have a
-  # filename but not a blob and need to figure out the language of the file.
-  class Pathname
-    # Public: Initialize a Pathname
-    #
-    # path - A filename String. The file may or maybe actually exist.
-    #
-    # Returns a Pathname.
-    def initialize(path)
-      @path = path
-    end
-
-    # Public: Get the basename of the path
-    #
-    # Examples
-    #
-    #   Pathname.new('sub/dir/file.rb').basename
-    #   # => 'file.rb'
-    #
-    # Returns a String.
-    def basename
-      File.basename(@path)
-    end
-
-    # Public: Get the extname of the path
-    #
-    # Examples
-    #
-    #   Pathname.new('.rb').extname
-    #   # => '.rb'
-    #
-    #   Pathname.new('file.rb').extname
-    #   # => '.rb'
-    #
-    # Returns a String.
-    def extname
-      File.extname(@path)
-    end
-
-    # Public: Get the language of the path
-    #
-    # The path extension name is the only heuristic used to detect the
-    # language name.
-    #
-    # Examples
-    #
-    #   Pathname.new('file.rb').language
-    #   # => Language['Ruby']
-    #
-    # Returns a Language or nil if none was found.
-    def language
-      @language ||= Language.find_by_filename(@path)
-    end
-
-    # Internal: Get the lexer of the path
-    #
-    # Returns a Lexer.
-    def lexer
-      language ? language.lexer : Pygments::Lexer.find_by_name('Text only')
-    end
-
-    # Public: Get the mime type
-    #
-    # Examples
-    #
-    #   Pathname.new('index.html').mime_type
-    #   # => 'text/html'
-    #
-    # Returns a mime type String.
-    def mime_type
-      @mime_type ||= Mime.mime_for(extname)
-    end
-
-    # Public: Return self as String
-    #
-    # Returns a String
-    def to_s
-      @path.dup
-    end
-
-    def eql?(other)
-      other.is_a?(self.class) && @path == other.to_s
-    end
-    alias_method :==, :eql?
-  end
-end

lib/linguist/repository.rb

@@ -80,7 +80,7 @@ module Linguist
       end
 
       # Compute total size
-      @size = @sizes.inject(0) { |s,(k,v)| s + v }
+      @size = @sizes.inject(0) { |s,(_,v)| s + v }
 
       # Get primary language
       if primary = @sizes.max_by { |(_, size)| size }

lib/linguist/sample.rb

@@ -1,74 +0,0 @@
-require 'linguist/classifier'
-require 'linguist/language'
-
-module Linguist
-  # Model for accessing classifier training data.
-  class Sample
-    # Samples live in test/ for now, we'll eventually move them out
-    PATH = File.expand_path("../../../test/fixtures", __FILE__)
-
-    # Public: Iterate over each Sample.
-    #
-    # &block - Yields Sample to block
-    #
-    # Returns nothing.
-    def self.each(&block)
-      Dir.entries(PATH).each do |category|
-        next if category == '.' || category == '..'
-
-        # Skip text and binary for now
-        # Possibly reconsider this later
-        next if category == 'text' || category == 'binary'
-
-        # Map directory name to a Language alias
-        language = Linguist::Language.find_by_alias(category)
-        raise "No language for #{category.inspect}" unless language
-
-        dirname = File.join(PATH, category)
-        Dir.entries(dirname).each do |filename|
-          next if filename == '.' || filename == '..'
-          yield new(File.join(dirname, filename), language)
-        end
-      end
-
-      nil
-    end
-
-    # Public: Build Classifier from all samples.
-    #
-    # Returns trained Classifier.
-    def self.classifier
-      classifier = Classifier.new
-      each { |sample| classifier.train(sample.language, sample.data) }
-      classifier.gc
-    end
-
-    # Internal: Initialize Sample.
-    #
-    # Samples should be initialized by Sample.each.
-    #
-    # path     - String full path to file.
-    # language - Language of sample.
-    def initialize(path, language)
-      @path     = path
-      @language = language
-    end
-
-    # Public: Get full path to file.
-    #
-    # Returns String.
-    attr_reader :path
-
-    # Public: Get sample language.
-    #
-    # Returns Language.
-    attr_reader :language
-
-    # Public: Read file contents.
-    #
-    # Returns String.
-    def data
-      File.read(path)
-    end
-  end
-end

lib/linguist/samples.rb

@@ -0,0 +1,94 @@
+require 'yaml'
+
+require 'linguist/md5'
+require 'linguist/classifier'
+
+module Linguist
+  # Model for accessing classifier training data.
+  module Samples
+    # Path to samples root directory
+    ROOT = File.expand_path("../../../samples", __FILE__)
+
+    # Path for serialized samples db
+    PATH = File.expand_path('../samples.json', __FILE__)
+
+    # Hash of serialized samples object
+    if File.exist?(PATH)
+      DATA = YAML.load_file(PATH)
+    end
+
+    # Public: Iterate over each sample.
+    #
+    # &block - Yields Sample to block
+    #
+    # Returns nothing.
+    def self.each(&block)
+      Dir.entries(ROOT).each do |category|
+        next if category == '.' || category == '..'
+
+        # Skip text and binary for now
+        # Possibly reconsider this later
+        next if category == 'Text' || category == 'Binary'
+
+        dirname = File.join(ROOT, category)
+        Dir.entries(dirname).each do |filename|
+          next if filename == '.' || filename == '..'
+
+          if filename == 'filenames'
+            Dir.entries(File.join(dirname, filename)).each do |subfilename|
+              next if subfilename == '.' || subfilename == '..'
+
+              yield({
+                :path    => File.join(dirname, filename, subfilename),
+                :language => category,
+                :filename => subfilename
+              })
+            end
+          else
+            yield({
+              :path     => File.join(dirname, filename),
+              :language => category,
+              :extname  => File.extname(filename)
+            })
+          end
+        end
+      end
+
+      nil
+    end
+
+    # Public: Build Classifier from all samples.
+    #
+    # Returns trained Classifier.
+    def self.data
+      db = {}
+      db['extnames'] = {}
+      db['filenames'] = {}
+
+      each do |sample|
+        language_name = sample[:language]
+
+        # TODO: For now skip empty extnames
+        if sample[:extname] && sample[:extname] != ""
+          db['extnames'][language_name] ||= []
+          if !db['extnames'][language_name].include?(sample[:extname])
+            db['extnames'][language_name] << sample[:extname]
+          end
+        end
+
+        # TODO: For now skip empty extnames
+        if fn = sample[:filename]
+          db['filenames'][language_name] ||= []
+          db['filenames'][language_name] << fn
+        end
+
+        data = File.read(sample[:path])
+        Classifier.train!(db, language_name, data)
+      end
+
+      db['md5'] = Linguist::MD5.hexdigest(db)
+
+      db
+    end
+  end
+end

lib/linguist/tokenizer.rb

@@ -5,25 +5,36 @@ module Linguist
   # It strips any data strings or comments and preserves significant
   # language symbols.
   class Tokenizer
-    # Public: Initialize a Tokenizer.
+    # Public: Extract tokens from data
     #
-    # data - String data to scan.
-    def initialize(data)
-      @data = data
-    end
-
-    # Public: Get source data.
-    #
-    # Returns String.
-    attr_reader :data
-
-    # Public: Extract tokens from data.
+    # data - String to tokenize
     #
     # Returns Array of token Strings.
-    def tokens
-      extract_tokens(data)
+    def self.tokenize(data)
+      new.extract_tokens(data)
     end
 
+    SINGLE_LINE_COMMENTS = [
+      '//', # C
+      '#',  # Ruby
+      '%',  # Tex
+    ]
+
+    MULTI_LINE_COMMENTS = [
+      ['/*', '*/'],    # C
+      ['<!--', '-->'], # XML
+      ['{-', '-}'],    # Haskell
+      ['(*', '*)']     # Coq
+    ]
+
+    START_SINGLE_LINE_COMMENT =  Regexp.compile(SINGLE_LINE_COMMENTS.map { |c|
+      "^\s*#{Regexp.escape(c)} "
+    }.join("|"))
+
+    START_MULTI_LINE_COMMENT =  Regexp.compile(MULTI_LINE_COMMENTS.map { |c|
+      Regexp.escape(c[0])
+    }.join("|"))
+
     # Internal: Extract generic tokens from data.
     #
     # data - String to scan.
@@ -39,38 +50,17 @@ module Linguist
 
       tokens = []
       until s.eos?
-        # Ruby single line comment
-        if token = s.scan(/# /)
-          tokens << "#"
+        # Single line comment
+        if token = s.scan(START_SINGLE_LINE_COMMENT)
+          tokens << token.strip
           s.skip_until(/\n|\Z/)
 
-        # C style single line comment
-        elsif token = s.scan(/\/\/ /)
-          tokens << "//"
-          s.skip_until(/\n|\Z/)
-
-        # Leading Tex or Matlab comments
-        elsif token = s.scan(/\n%/)
-          tokens << "%"
-          s.skip_until(/\n|\Z/)
-
-        # C multiline comments
-        elsif token = s.scan(/\/\*/)
-          tokens << "/*"
-          s.skip_until(/\*\//)
-          tokens << "*/"
-
-        # Haskell multiline comments
-        elsif token = s.scan(/\{-/)
-          tokens << "{-"
-          s.skip_until(/-\}/)
-          tokens << "-}"
-
-        # XML multiline comments
-        elsif token = s.scan(/<!--/)
-          tokens << "<!--"
-          s.skip_until(/-->/)
-          tokens << "-->"
+        # Multiline comments
+        elsif token = s.scan(START_MULTI_LINE_COMMENT)
+          tokens << token
+          close_token = MULTI_LINE_COMMENTS.assoc(token)[1]
+          s.skip_until(Regexp.compile(Regexp.escape(close_token)))
+          tokens << close_token
 
         # Skip single or double quoted strings
         elsif s.scan(/"/)

samples/Ceylon/Foo.ceylon

@@ -0,0 +1,15 @@
+doc "Test function for Ceylon"
+by  "Enrique"
+shared void test() {
+  print("test");
+}
+
+doc "Test class for Ceylon"
+shared class Test(name) satisfies Comparable<Test> {
+    shared String name;
+    shared actual String string = "Test " name ".";
+
+    shared actual Comparison compare(Test other) {
+        return name<=>other.name;
+    }
+}

samples/Coq/Basics.v

@@ -0,0 +1,707 @@
+Inductive day : Type :=
+| monday : day
+| tuesday : day
+| wednesday : day
+| thursday : day
+| friday : day
+| saturday : day
+| sunday : day.
+
+Definition next_weekday (d:day) : day :=
+  match d with
+  | monday => tuesday
+  | tuesday => wednesday
+  | wednesday => thursday
+  | thursday => friday
+  | friday => monday
+  | saturday => monday
+  | sunday => monday
+  end.
+
+Example test_next_weekday:
+(next_weekday (next_weekday saturday)) = tuesday.
+
+Proof. simpl. reflexivity. Qed.
+
+Inductive bool : Type :=
+	| true : bool
+	| false : bool.
+
+Definition negb (b:bool) : bool :=
+													 match b with
+																			 | true => false
+																			 | false => true
+													 end.
+
+Definition andb (b1:bool) (b2:bool) : bool :=
+		match b1 with
+		 | true => b2
+		 | false => false
+	  end.
+
+Definition orb (b1:bool) (b2:bool) : bool :=
+		match b1 with
+		  | true => true
+		  | false => b2
+		end.
+
+Example test_orb1: (orb true false) = true.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb2: (orb false false) = false.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb3: (orb false true) = true.
+Proof. simpl. reflexivity. Qed.
+
+Example test_orb4: (orb true true) = true.
+Proof. simpl. reflexivity. Qed.
+
+Definition nandb (b1: bool) (b2:bool) : bool :=
+	match b1 with
+		| true => match b2 with
+										| false => true
+										| true => false
+							end
+		| false => true
+	end.
+
+Example test_nandb1: (nandb true false) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb2: (nandb false false) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb3: (nandb false true) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_nandb4: (nandb true true) = false.
+Proof. simpl. reflexivity. Qed.
+
+Definition andb3 (b1: bool) (b2:bool) (b3:bool) : bool :=
+	match b1 with
+    | false => false
+		| true => match b2 with
+								| false => false
+								| true => b3
+							end
+	end.
+
+Example test_andb31: (andb3 true true true) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_andb32: (andb3 false true true) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_andb33: (andb3 true false true) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_andb34: (andb3 true true false) = false.
+Proof. simpl. reflexivity. Qed.
+
+Module Playground1.
+
+Inductive nat : Type :=
+	| O : nat
+	| S : nat -> nat.
+
+Definition pred (n : nat) : nat :=
+	match n with
+		| O => O
+		| S n' => n'
+	end.
+
+Definition minustwo (n : nat) : nat :=
+	match n with
+		| O => O
+		| S O => O
+		| S (S n') => n'
+	end.
+
+Fixpoint evenb (n : nat) : bool :=
+	match n with
+		| O => true
+		| S O => false
+		| S (S n') => evenb n'
+	end.
+
+Definition oddb (n : nat) : bool := negb (evenb n).
+
+Example test_oddb1: (oddb (S O)) = true.
+Proof. reflexivity. Qed.
+Example test_oddb2: (oddb (S (S (S (S O))))) = false.
+Proof. reflexivity. Qed.
+
+Fixpoint plus (n : nat) (m : nat) : nat :=
+	match n with
+		| O => m
+		| S n' => S (plus n' m)
+	end.
+
+Fixpoint mult (n m : nat) : nat :=
+	match n with
+		| O => O
+		| S n' => plus m (mult n' m)
+	end.
+
+Fixpoint minus (n m : nat) : nat :=
+	match n, m with
+		| O, _ => n
+		| S n', O => S n'
+		| S n', S m' => minus n' m'
+	end.
+
+Fixpoint exp (base power : nat) : nat :=
+	match power with
+		| O => S O
+		| S p => mult base (exp base p)
+	end.
+
+Fixpoint factorial (n : nat) : nat :=
+	match n with
+		| O => S O
+		| S n' => mult n (factorial n')
+	end.
+
+Example test_factorial1: (factorial (S (S (S O)))) = (S (S (S (S (S (S O)))))).
+Proof. simpl. reflexivity. Qed.
+
+Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
+Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope.
+Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope.
+
+Fixpoint beq_nat (n m : nat) : bool :=
+	match n with
+		| O => match m with
+						| O => true
+						| S m' => false
+					 end
+		| S n' => match m with
+							| O => false
+							| S m' => beq_nat n' m'
+							end
+	end.
+
+Fixpoint ble_nat (n m : nat) : bool :=
+	match n with
+		| O => true
+		| S n' => 
+				match m with
+					| O => false
+					| S m' => ble_nat n' m'
+				end
+	end.
+
+Example test_ble_nat1: (ble_nat (S (S O)) (S (S O))) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_ble_nat2: (ble_nat (S (S O)) (S (S (S (S O))))) = true.
+Proof. simpl. reflexivity. Qed.
+Example test_ble_nat3: (ble_nat (S (S (S (S O)))) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+
+Definition blt_nat (n m : nat) : bool :=
+		(andb (negb (beq_nat n m)) (ble_nat n m)).
+
+Example test_blt_nat1: (blt_nat (S (S O)) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_blt_nat3: (blt_nat (S (S (S (S O)))) (S (S O))) = false.
+Proof. simpl. reflexivity. Qed.
+Example test_blt_nat2 : (blt_nat (S (S O)) (S (S (S (S O))))) = true.
+Proof. simpl. reflexivity. Qed.
+
+Theorem plus_O_n : forall n : nat, O + n = n.
+Proof.
+	simpl. reflexivity. Qed.
+
+Theorem plus_O_n' : forall n : nat, O + n = n.
+Proof.
+	reflexivity. Qed.
+
+Theorem plus_O_n'' : forall n : nat, O + n = n.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem plus_1_1 : forall n : nat, (S O) + n = S n.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem mult_0_1: forall n : nat, O * n = O.
+Proof.
+	intros n. reflexivity. Qed.
+
+Theorem plus_id_example : forall n m:nat,
+	n = m -> n + n = m + m.
+Proof.
+	intros n m.
+	intros H.
+	rewrite -> H.
+	reflexivity. Qed.
+
+Theorem plus_id_exercise : forall n m o: nat,
+	n = m -> m = o -> n + m = m + o.
+Proof.
+	intros n m o.
+	intros H.
+	intros H'.
+	rewrite -> H.
+	rewrite <- H'.
+	reflexivity.
+	Qed.
+
+Theorem mult_0_plus : forall n m : nat,
+				(O + n) * m = n * m.
+Proof.
+	intros n m.
+	rewrite -> plus_O_n.
+	reflexivity. Qed.
+
+Theorem mult_1_plus : forall n m: nat,
+	((S O) + n) * m = m + (n * m).
+Proof.
+	intros n m.
+	rewrite -> plus_1_1.
+	reflexivity.
+	Qed.
+
+Theorem mult_1 : forall n : nat,
+				n * (S O) = n.
+Proof.
+	intros n.
+	induction n as [| n'].
+	reflexivity.
+	simpl.
+	rewrite -> IHn'.
+	reflexivity.
+	Qed.
+
+Theorem plus_1_neq_0 : forall n : nat,
+				beq_nat (n + (S O)) O = false.
+Proof.
+	intros n.
+	destruct n as [| n'].
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem zero_nbeq_plus_1 : forall n : nat,
+				beq_nat O (n + (S O)) = false.
+Proof.
+	intros n.
+	destruct n.
+	reflexivity.
+	reflexivity.
+Qed.
+
+Require String. Open Scope string_scope.
+
+Ltac move_to_top x :=
+match reverse goal with
+| H : _ |- _ => try move x after H
+end.
+
+Tactic Notation "assert_eq" ident(x) constr(v) :=
+	let H := fresh in
+	assert (x = v) as H by reflexivity;
+	clear H.
+
+	Tactic Notation "Case_aux" ident(x) constr(name) :=
+		first [
+		set (x := name); move_to_top x
+		| assert_eq x name; move_to_top x
+		| fail 1 "because we are working on a different case" ].
+
+		Ltac Case name := Case_aux Case name.
+		Ltac SCase name := Case_aux SCase name.
+		Ltac SSCase name := Case_aux SSCase name.
+		Ltac SSSCase name := Case_aux SSSCase name.
+		Ltac SSSSCase name := Case_aux SSSSCase name.
+		Ltac SSSSSCase name := Case_aux SSSSSCase name.
+		Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
+		Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.
+
+Theorem andb_true_elim1 : forall b c : bool,
+				andb b c = true -> b = true.
+Proof.
+	intros b c H.
+	destruct b.
+	Case "b = true".
+		reflexivity.
+	Case "b = false".
+		rewrite <- H. reflexivity. Qed.
+
+Theorem plus_0_r : forall n : nat, n + O = n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0". reflexivity.
+	Case "n = S n'". simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem minus_diag : forall n,
+				minus n n = O.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		simpl. reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+
+Theorem mult_0_r : forall n:nat,
+				n * O = O.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem plus_n_Sm : forall n m : nat,
+				S (n + m) = n + (S m).
+Proof.
+	intros n m. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem plus_assoc : forall n m p : nat,
+					n + (m + p) = (n + m) + p.
+Proof.
+	intros n m p.
+	induction n as [| n'].
+	reflexivity.
+	simpl.
+	rewrite -> IHn'.
+	reflexivity. Qed.
+
+Theorem plus_distr : forall n m: nat, S (n + m) = n + (S m).
+Proof.
+	intros n m.  induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem mult_distr : forall n m: nat, n * ((S O) + m) = n * (S m).
+Proof.
+	intros n m.
+	induction n as [| n'].
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem plus_comm : forall n m : nat,
+	n + m = m + n.
+Proof.
+	intros n m.
+	induction n as [| n'].
+	Case "n = 0".
+		simpl.
+		rewrite -> plus_0_r.
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		rewrite -> IHn'.
+		rewrite -> plus_distr.
+		reflexivity. Qed.
+
+Fixpoint double (n:nat) :=
+	match n with
+		| O => O
+		| S n' => S (S (double n'))
+	end.
+
+Lemma double_plus : forall n, double n = n + n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n'".
+		simpl. rewrite -> IHn'.
+		rewrite -> plus_distr. reflexivity.
+		Qed.
+
+Theorem beq_nat_refl : forall n : nat,
+	true = beq_nat n n.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n".
+		simpl. rewrite <- IHn'.
+		reflexivity. Qed.
+
+Theorem plus_rearrange: forall n m p q : nat,
+				(n + m) + (p + q) = (m + n) + (p + q).
+Proof.
+	intros n m p q.
+	assert(H: n + m = m + n).
+		Case "Proof by assertion".
+		rewrite -> plus_comm. reflexivity.
+	rewrite -> H. reflexivity. Qed.
+
+Theorem plus_swap : forall n m p: nat,
+				n + (m + p) = m + (n + p).
+Proof.
+	intros n m p.
+	rewrite -> plus_assoc.
+	assert(H: m + (n + p) = (m + n) + p).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H.
+	assert(H2: m + n = n + m).
+	rewrite -> plus_comm.
+	reflexivity.
+	rewrite -> H2.
+	reflexivity.
+	Qed.
+
+Theorem plus_swap' : forall n m p: nat,
+				n + (m + p) = m + (n + p).
+Proof.
+	intros n m p.
+	rewrite -> plus_assoc.
+	assert(H: m + (n + p) = (m + n) + p).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H.
+	replace (m + n) with (n + m).
+	rewrite -> plus_comm.
+	reflexivity.
+	rewrite -> plus_comm.
+	reflexivity.
+	Qed.
+
+Theorem mult_1_distr: forall m n: nat,
+				n * ((S O) + m) = n * (S O) + n * m.
+Proof.
+	intros n m.
+	rewrite -> mult_1.
+	rewrite -> plus_1_1.
+	simpl.
+	induction m as [|m'].
+	simpl.
+	reflexivity.
+	simpl.
+	rewrite -> plus_swap.
+	rewrite <- IHm'.
+	reflexivity.
+	Qed.
+
+Theorem mult_comm: forall m n : nat,
+				m * n = n * m.
+Proof.
+	intros m n.
+	induction n as [| n'].
+	Case "n = 0".
+		simpl.
+		rewrite -> mult_0_r.
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		rewrite <- mult_distr.
+		rewrite -> mult_1_distr.
+		rewrite -> mult_1.
+		rewrite -> IHn'.
+		reflexivity.
+		Qed.
+
+Theorem evenb_next : forall n : nat,
+				evenb n = evenb (S (S n)).
+Proof.
+	intros n.
+Admitted.
+
+Theorem negb_negb : forall n : bool,
+				n = negb (negb n).
+Proof.
+	intros n.
+	destruct n.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem evenb_n_oddb_Sn : forall n : nat,
+				evenb n = negb (evenb (S n)).
+Proof.
+	intros n.
+	induction n as [|n'].
+	reflexivity.
+	assert(H: evenb n' = evenb (S (S n'))).
+	reflexivity.
+	rewrite <- H.
+	rewrite -> IHn'.
+	rewrite <- negb_negb.
+	reflexivity.
+	Qed.
+
+(*Fixpoint bad (n : nat) : bool :=
+	match n with
+		| O => true
+		| S O => bad (S n)
+		| S (S n') => bad n'
+	end.*)
+
+Theorem ble_nat_refl : forall n:nat,
+				true = ble_nat n n.
+Proof.
+	intros n.
+	induction n as [|n'].
+	Case "n = 0".
+		reflexivity.
+	Case "n = S n".
+		simpl.
+		rewrite <- IHn'.
+		reflexivity.
+	Qed.
+
+Theorem zero_nbeq_S : forall n: nat,
+				beq_nat O (S n) = false.
+Proof.
+	intros n.
+	reflexivity.
+	Qed.
+
+Theorem andb_false_r : forall b : bool,
+				andb b false = false.
+Proof.
+	intros b.
+	destruct b.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem plus_ble_compat_1 : forall n m p : nat,
+				ble_nat n m = true -> ble_nat (p + n) (p + m) = true.
+Proof.
+	intros n m p.
+	intros H.
+	induction p.
+	Case "p = 0".
+		simpl.
+		rewrite -> H.
+		reflexivity.
+	Case "p = S p'".
+		simpl.
+		rewrite -> IHp.
+		reflexivity.
+		Qed.
+
+Theorem S_nbeq_0 : forall n:nat,
+				beq_nat (S n) O = false.
+Proof.
+	intros n.
+	reflexivity.
+	Qed.
+
+Theorem mult_1_1 : forall n:nat, (S O) * n = n.
+Proof.
+	intros n.
+	simpl.
+	rewrite -> plus_0_r.
+	reflexivity. Qed.
+
+Theorem all3_spec : forall b c : bool,
+	orb (andb b c)
+			(orb (negb b)
+			 		 (negb c))
+	= true.
+Proof.
+	intros b c.
+	destruct b.
+	destruct c.
+	reflexivity.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Lemma mult_plus_1 : forall n m : nat,
+			S(m + n) = m + (S n).
+Proof.
+	intros n m.
+	induction m.
+	reflexivity.
+	simpl.
+	rewrite -> IHm.
+	reflexivity.
+	Qed.
+
+Theorem mult_mult : forall n m : nat,
+	n * (S m) = n * m + n.
+Proof.
+	intros n m.
+	induction n.
+	reflexivity.
+	simpl.
+	rewrite -> IHn.
+	rewrite -> plus_assoc.
+	rewrite -> mult_plus_1.
+	reflexivity.
+	Qed.
+
+Theorem mult_plus_distr_r : forall n m p:nat,
+				(n + m) * p = (n * p) + (m * p).
+Proof.
+	intros n m p.
+	induction p.
+	rewrite -> mult_0_r.
+	rewrite -> mult_0_r.
+	rewrite -> mult_0_r.
+	reflexivity.
+	rewrite -> mult_mult.
+	rewrite -> mult_mult.
+	rewrite -> mult_mult.
+	rewrite -> IHp.
+	assert(H1: ((n * p) + n) + (m * p + m) = (n * p) + (n + (m * p + m))).
+	rewrite <- plus_assoc.
+	reflexivity.
+	rewrite -> H1.
+	assert(H2: (n + (m * p + m)) = (m * p + (n + m))).
+	rewrite -> plus_swap.
+	reflexivity.
+	rewrite -> H2.
+	assert(H3: (n * p) + (m * p + (n + m)) = ((n * p ) + (m * p)) + (n + m)).
+	rewrite -> plus_assoc.
+	reflexivity.
+	rewrite -> H3.
+	reflexivity.
+	Qed.
+
+Theorem mult_assoc : forall n m p : nat,
+				n * (m * p) = (n * m) * p.
+Proof.
+	intros n m p.
+	induction n.
+	simpl.
+	reflexivity.
+	simpl.
+	rewrite -> mult_plus_distr_r.
+	rewrite -> IHn.
+	reflexivity.
+	Qed.
+
+Inductive bin : Type :=
+	| BO : bin
+	| D : bin -> bin
+	| M : bin -> bin.
+
+Fixpoint incbin (n : bin) : bin :=
+	match n with
+		| BO => M (BO)
+		| D n' => M n'
+		| M n' => D (incbin n')
+	end.
+
+Fixpoint bin2un (n : bin) : nat :=
+	match n with
+		| BO => O
+		| D n' => double (bin2un n')
+		| M n' => S (double (bin2un n'))
+	end.
+
+Theorem bin_comm : forall n : bin,
+				bin2un(incbin n) = S (bin2un n).
+Proof.
+	intros n.
+	induction n.
+		reflexivity.
+		reflexivity.
+		simpl.
+		rewrite -> IHn.
+		reflexivity.
+	Qed.
+
+End Playground1.

samples/Coq/Heap.v

@@ -0,0 +1,300 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
+
+(** A development of Treesort on Heap trees. It has an average
+    complexity of O(n.log n) but of O(n²) in the worst case (e.g. if
+    the list is already sorted) *)
+
+(* G. Huet 1-9-95 uses Multiset *)
+
+Require Import List Multiset PermutSetoid Relations Sorting.
+
+Section defs.
+
+  (** * Trees and heap trees *)
+
+  (** ** Definition of trees over an ordered set *)
+
+  Variable A : Type.
+  Variable leA : relation A.
+  Variable eqA : relation A.
+
+  Let gtA (x y:A) := ~ leA x y.
+
+  Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+  Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+  Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+  Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
+
+  Hint Resolve leA_refl.
+  Hint Immediate eqA_dec leA_dec leA_antisym.
+
+  Let emptyBag := EmptyBag A.
+  Let singletonBag := SingletonBag _ eqA_dec.
+
+  Inductive Tree :=
+    | Tree_Leaf : Tree
+    | Tree_Node : A -> Tree -> Tree -> Tree.
+
+  (** [a] is lower than a Tree [T] if [T] is a Leaf
+      or [T] is a Node holding [b>a] *)
+
+  Definition leA_Tree (a:A) (t:Tree) :=
+    match t with
+      | Tree_Leaf => True
+      | Tree_Node b T1 T2 => leA a b
+    end.
+
+  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
+  Proof.
+    simpl; auto with datatypes.
+  Qed.
+
+  Lemma leA_Tree_Node :
+    forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
+  Proof.
+    simpl; auto with datatypes.
+  Qed.
+
+
+  (** ** The heap property *)
+
+  Inductive is_heap : Tree -> Prop :=
+    | nil_is_heap : is_heap Tree_Leaf
+    | node_is_heap :
+      forall (a:A) (T1 T2:Tree),
+        leA_Tree a T1 ->
+        leA_Tree a T2 ->
+        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
+
+  Lemma invert_heap :
+    forall (a:A) (T1 T2:Tree),
+      is_heap (Tree_Node a T1 T2) ->
+      leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
+  Proof.
+    intros; inversion H; auto with datatypes.
+  Qed.
+
+  (* This lemma ought to be generated automatically by the Inversion tools *)
+  Lemma is_heap_rect :
+    forall P:Tree -> Type,
+      P Tree_Leaf ->
+      (forall (a:A) (T1 T2:Tree),
+	leA_Tree a T1 ->
+	leA_Tree a T2 ->
+	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+      forall T:Tree, is_heap T -> P T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros a G PG D PD PN.
+    elim (invert_heap a G D); auto with datatypes.
+    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+    apply X0; auto with datatypes.
+  Qed.
+
+  (* This lemma ought to be generated automatically by the Inversion tools *)
+  Lemma is_heap_rec :
+    forall P:Tree -> Set,
+      P Tree_Leaf ->
+      (forall (a:A) (T1 T2:Tree),
+	leA_Tree a T1 ->
+	leA_Tree a T2 ->
+	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+      forall T:Tree, is_heap T -> P T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros a G PG D PD PN.
+    elim (invert_heap a G D); auto with datatypes.
+    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+    apply X; auto with datatypes.
+  Qed.
+
+  Lemma low_trans :
+    forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros; simpl; apply leA_trans with b; auto with datatypes.
+  Qed.
+
+  (** ** Merging two sorted lists *)
+
+  Inductive merge_lem (l1 l2:list A) : Type :=
+    merge_exist :
+    forall l:list A,
+      Sorted leA l ->
+      meq (list_contents _ eqA_dec l)
+      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
+      (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
+      merge_lem l1 l2.
+  Require Import Morphisms.
+  
+  Instance: Equivalence (@meq A).
+  Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
+
+  Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
+  Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
+  
+  Lemma merge :
+    forall l1:list A, Sorted leA l1 ->
+    forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
+  Proof.
+    fix 1; intros; destruct l1.
+    apply merge_exist with l2; auto with datatypes.
+    rename l1 into l.
+    revert l2 H0. fix 1. intros.
+    destruct l2 as [|a0 l0]. 
+    apply merge_exist with (a :: l); simpl; auto with datatypes. 
+    elim (leA_dec a a0); intros.
+
+    (* 1 (leA a a0) *)
+    apply Sorted_inv in H. destruct H.
+    destruct (merge l H (a0 :: l0) H0).
+    apply merge_exist with (a :: l1). clear merge merge0.
+      auto using cons_sort, cons_leA with datatypes.
+    simpl. rewrite m. now rewrite munion_ass. 
+    intros. apply cons_leA. 
+    apply (@HdRel_inv _ leA) with l; trivial with datatypes.
+
+    (* 2 (leA a0 a) *)
+    apply Sorted_inv in H0. destruct H0.
+    destruct (merge0 l0 H0). clear merge merge0.  
+    apply merge_exist with (a0 :: l1); 
+      auto using cons_sort, cons_leA with datatypes.
+    simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
+    repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
+    intros. apply cons_leA. 
+    apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
+  Qed.
+
+  (** ** From trees to multisets *)
+
+  (** contents of a tree as a multiset *)
+
+  (** Nota Bene : In what follows the definition of SingletonBag
+      in not used. Actually, we could just take as postulate:
+      [Parameter SingletonBag : A->multiset].  *)
+
+  Fixpoint contents (t:Tree) : multiset A :=
+    match t with
+      | Tree_Leaf => emptyBag
+      | Tree_Node a t1 t2 =>
+	munion (contents t1) (munion (contents t2) (singletonBag a))
+    end.
+
+
+  (** equivalence of two trees is equality of corresponding multisets *)
+  Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
+
+
+
+  (** * From lists to sorted lists *)
+
+  (** ** Specification of heap insertion *)
+
+  Inductive insert_spec (a:A) (T:Tree) : Type :=
+    insert_exist :
+    forall T1:Tree,
+      is_heap T1 ->
+      meq (contents T1) (munion (contents T) (singletonBag a)) ->
+      (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
+      insert_spec a T.
+
+
+  Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
+  Proof.
+    simple induction 1; intros.
+    apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    simpl; unfold meq, munion; auto using node_is_heap with datatypes.
+    elim (leA_dec a a0); intros.
+    elim (X a0); intros.
+    apply insert_exist with (Tree_Node a T2 T0);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    simpl; apply treesort_twist1; trivial with datatypes.
+    elim (X a); intros T3 HeapT3 ConT3 LeA.
+    apply insert_exist with (Tree_Node a0 T2 T3);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    apply low_trans with a; auto with datatypes.
+    apply LeA; auto with datatypes.
+    apply low_trans with a; auto with datatypes.
+    simpl; apply treesort_twist2; trivial with datatypes.
+  Qed.
+
+
+  (** ** Building a heap from a list *)
+
+  Inductive build_heap (l:list A) : Type :=
+    heap_exist :
+    forall T:Tree,
+      is_heap T ->
+      meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
+
+  Lemma list_to_heap : forall l:list A, build_heap l.
+  Proof.
+    simple induction l.
+    apply (heap_exist nil Tree_Leaf); auto with datatypes.
+    simpl; unfold meq; exact nil_is_heap.
+    simple induction 1.
+    intros T i m; elim (insert T i a).
+    intros; apply heap_exist with T1; simpl; auto with datatypes.
+    apply meq_trans with (munion (contents T) (singletonBag a)).
+    apply meq_trans with (munion (singletonBag a) (contents T)).
+    apply meq_right; trivial with datatypes.
+    apply munion_comm.
+    apply meq_sym; trivial with datatypes.
+  Qed.
+
+
+  (** ** Building the sorted list *)
+
+  Inductive flat_spec (T:Tree) : Type :=
+    flat_exist :
+    forall l:list A,
+      Sorted leA l ->
+      (forall a:A, leA_Tree a T -> HdRel leA a l) ->
+      meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
+
+  Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
+  Proof.
+    intros T h; elim h; intros.
+    apply flat_exist with (nil (A:=A)); auto with datatypes.
+    elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
+    elim (merge _ s1 _ s2); intros.
+    apply flat_exist with (a :: l); simpl; auto with datatypes.
+    apply meq_trans with
+      (munion (list_contents _ eqA_dec l1)
+	(munion (list_contents _ eqA_dec l2) (singletonBag a))).
+    apply meq_congr; auto with datatypes.
+    apply meq_trans with
+      (munion (singletonBag a)
+	(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
+    apply munion_rotate.
+    apply meq_right; apply meq_sym; trivial with datatypes.
+  Qed.
+
+
+  (** * Specification of treesort *)
+
+  Theorem treesort :
+    forall l:list A,
+    {m : list A | Sorted leA m & permutation _ eqA_dec l m}.
+  Proof.
+    intro l; unfold permutation.
+    elim (list_to_heap l).
+    intros.
+    elim (heap_to_list T); auto with datatypes.
+    intros.
+    exists l0; auto with datatypes.
+    apply meq_trans with (contents T); trivial with datatypes.
+  Qed.
+
+End defs.

samples/Coq/Lists.v

@@ -0,0 +1,591 @@
+Require Export Basics.
+Module NatList.
+Import Playground1.
+
+Inductive natprod : Type :=
+	pair : nat -> nat -> natprod.
+
+Definition fst (p : natprod) : nat :=
+	match p with
+		| pair x y => x
+	end.
+
+Definition snd (p : natprod) : nat :=
+	match p with
+		| pair x y => y
+	end.
+
+Notation "( x , y )" := (pair x y).
+
+Definition swap_pair (p : natprod) : natprod :=
+	match p with
+			| (x, y) => (y, x)
+	end.
+
+Theorem surjective_pairing' : forall (n m : nat),
+	(n, m) = (fst (n, m), snd (n, m)).
+Proof.
+	reflexivity.  Qed.
+
+Theorem surjective_pairing : forall (p : natprod),
+	p = (fst p, snd p).
+Proof.
+	intros p.
+	destruct p as (n, m).
+	simpl.
+	reflexivity.
+	Qed.
+
+Theorem snd_fst_is_swap : forall (p : natprod),
+	(snd p, fst p) = swap_pair p.
+Proof.
+	intros p.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Theorem fst_swap_is_snd : forall (p : natprod),
+	 fst (swap_pair p) = snd p.
+Proof.
+	intros p.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Inductive natlist : Type :=
+	| nil : natlist
+	| cons : nat -> natlist -> natlist.
+
+Definition l_123 := cons (S O) (cons (S (S O)) (cons (S (S (S O))) nil)).
+
+Notation "x :: l" := (cons x l) (at level 60, right associativity).
+Notation "[ ]" := nil.
+Notation "[]" := nil.
+Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
+
+Fixpoint repeat (n count : nat) : natlist :=
+	match count with
+		| O => nil
+		| S count' => n :: (repeat n count')
+	end.
+
+Fixpoint length (l:natlist) : nat :=
+	match l with
+		| nil => O
+		| h :: t => S (length t)
+	end.
+
+Fixpoint app (l1 l2 : natlist) : natlist :=
+	match l1 with
+		| nil => l2
+		| h :: t => h :: (app t l2)
+	end.
+
+Notation "x ++ y" := (app x y) (right associativity, at level 60).
+
+(*
+Example test_app1: [1,2,3] ++ [4,5] = [1,2,3,4,5].
+Proof. reflexivity. Qed.
+Example test_app2: nil ++ [4,5] = [4,5].
+Proof. reflexivity. Qed.
+Example test_app3: [1,2,3] ++ [] = [1,2,3].
+Proof. reflexivity. Qed.
+*)
+
+Definition head (l : natlist) : nat :=
+	match l with
+		| nil => O
+		| h :: t => h
+	end.
+
+Definition tl (l : natlist) : natlist :=
+	match l with
+		| nil => nil
+		| h :: t => t
+	end.
+
+			(*
+Example test_tl: tl [1,2,3] = [2,3].
+Proof. reflexivity. Qed.
+*)
+
+Fixpoint nonzeros (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| O :: r => nonzeros r
+		| n :: r => n :: (nonzeros r)
+	end.
+
+Example test_nonzeros: nonzeros [O,S O,O,S (S O), S (S (S O)),O,O] = [S O,S (S O), S (S (S O))].
+Proof. reflexivity. Qed.
+
+Fixpoint oddmembers (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| n :: r => match (oddb n) with
+										| true => n :: (oddmembers r)
+										| false => oddmembers r
+								end
+	end.
+
+Example test_oddmembers: oddmembers [O, S O, O, S (S O), S (S (S O)), O, O] = [S O, S (S (S O))].
+Proof. reflexivity. Qed.
+
+Fixpoint countoddmembers (l:natlist) : nat :=
+		length (oddmembers l).
+
+Example test_countoddmembers2: countoddmembers [O, S (S O), S (S (S (S O)))] = O.
+Proof. reflexivity. Qed.
+
+Example test_countoddmembers3: countoddmembers [] = O.
+Proof. reflexivity. Qed.
+
+Fixpoint alternate (l1 l2 : natlist) : natlist :=
+		match l1 with
+				| nil => l2
+				| a :: r1 => match l2 with
+											| nil => l1
+											| b :: r2 => a :: b :: (alternate r1 r2)
+										end
+		end.
+
+Example test_alternative1: alternate [S O, S (S O), S (S (S O))] [S (S (S (S O))), S (S (S (S (S O)))), S (S (S (S (S (S O)))))] =
+		[S O, S (S (S (S O))), S (S O), S (S (S (S (S O)))), S (S (S O)), S (S (S (S (S (S O)))))].
+Proof. reflexivity. Qed.
+
+Definition bag := natlist.
+
+Fixpoint count (v : nat) (s: bag) : nat :=
+	match s with
+		| nil => O
+		| v' :: r => match (beq_nat v' v) with
+										| true => S (count v r)
+										| false => count v r
+								 end
+	end.
+
+Example test_count1: count (S O) [S O, S (S O), S (S (S O)), S O, S (S (S (S O))), S O] = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition sum : bag -> bag -> bag := app.
+
+Example test_sum1: count (S O) (sum [S O, S (S O), S (S (S O))] [S O, S (S (S (S O))), S O]) = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition add (v:nat) (s:bag) : bag := v :: s.
+
+Example test_add1: count (S O) (add (S O) [S O, S (S (S (S O))), S O]) = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Definition member (v:nat) (s:bag) : bool :=
+	ble_nat (S O) (count v s).
+
+Example test_member1: member (S O) [S O, S (S (S (S O))), S O] = true.
+Proof. reflexivity. Qed.
+
+Example test_member2: member (S (S O)) [S O, S (S (S (S O))), S O] = false.
+Proof. reflexivity. Qed.
+
+Fixpoint remove_one (v:nat) (s:bag) : bag :=
+	match s with
+		| nil => nil
+		| v' :: r => match (beq_nat v v') with
+									| true => r
+									| false => v' :: (remove_one v r)
+								 end
+	end.
+
+Example test_remove_one1: count (S (S (S (S (S O)))))
+																(remove_one (S (S (S (S (S O)))))
+																[S (S O), S O, S (S (S (S (S O)))), S (S (S (S O))), S O]) = O.
+Proof. reflexivity. Qed.
+
+Fixpoint remove_all (v:nat) (s:bag) : bag :=
+	match s with
+		| nil => nil
+		| v' :: r => match (beq_nat v v') with
+										| true => remove_all v r
+										| false => v' :: (remove_all v r)
+								 end
+	end.
+
+Example test_remove_all1: count (S (S (S (S (S O)))))
+																(remove_all (S (S (S (S (S O)))))
+																[S (S O), S O, S (S (S (S (S O)))), S (S (S (S O))), S O]) = O.
+Proof. reflexivity. Qed.
+
+Fixpoint subset (s1:bag) (s2:bag) : bool :=
+		match s1 with
+			| nil => true
+			| v :: r => andb (member v s2)
+											 (subset r (remove_one v s2))
+		end.
+
+Definition test_subset1: subset [S O, S (S O)] [S (S O), S O, S (S (S (S O))), S O] = true.
+Proof. reflexivity. Qed.
+Definition test_subset2: subset [S O, S (S O), S (S O)] [S (S O), S O, S (S (S (S O))), S O] = false.
+Proof. reflexivity. Qed.
+
+Theorem bag_count_add : forall n t: nat, forall s : bag,
+				count n s = t -> count n (add n s) = S t.
+Proof.
+	intros n t s.
+	intros H.
+	induction s.
+	simpl.
+	rewrite <- beq_nat_refl.
+	rewrite <- H.
+	reflexivity.
+	rewrite <- H.
+	simpl.
+	rewrite <- beq_nat_refl.
+	reflexivity.
+Qed.
+
+Theorem nil_app : forall l:natlist,
+	[] ++ l = l.
+Proof.
+	reflexivity. Qed.
+
+Theorem tl_length_pred : forall l:natlist,
+	pred (length l) = length (tl l).
+Proof.
+	intros l. destruct l as [| n l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons n l'".
+		reflexivity. Qed.
+
+Theorem app_ass:forall l1 l2 l3 : natlist,
+	(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+Proof.
+	intros l1 l2 l3. induction l1 as [| n l1'].
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons n l1'".
+		simpl. rewrite -> IHl1'. reflexivity. Qed.
+
+Theorem app_length: forall l1 l2 : natlist,
+	length (l1 ++ l2) = (length l1) + (length l2).
+Proof.
+	intros l1 l2. induction l1 as [| n l1'].
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons".
+		simpl. rewrite -> IHl1'. reflexivity. Qed.
+
+Fixpoint snoc (l:natlist) (v:nat) : natlist :=
+	match l with
+		| nil => [v]
+		| h :: t => h :: (snoc t v)
+	end.
+
+Fixpoint rev (l:natlist) : natlist :=
+	match l with
+		| nil => nil
+		| h :: t => snoc (rev t) h
+	end.
+
+Example test_rev1: rev [S O, S (S O), S (S (S O))] = [S (S (S O)), S (S O), S O].
+Proof. reflexivity. Qed.
+
+Theorem length_snoc : forall n : nat, forall l : natlist,
+	length (snoc l n) = S (length l).
+Proof.
+	intros n l. induction l as [| n' l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons n' l'".
+		simpl. rewrite -> IHl'. reflexivity. Qed.
+
+Theorem rev_length : forall l : natlist,
+	length (rev l) = length l.
+Proof.
+	intros l. induction l as [| n l'].
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl. rewrite -> length_snoc.
+		rewrite -> IHl'. reflexivity. Qed.
+
+Theorem app_nil_end : forall l :natlist,
+	l ++ [] = l.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl. rewrite -> IHl. reflexivity. Qed.
+
+
+
+Theorem rev_snoc : forall l: natlist, forall n : nat,
+	rev (snoc l n) = n :: (rev l).
+Proof.
+	intros l n.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem rev_involutive : forall l : natlist,
+	rev (rev l) = l.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> rev_snoc.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem app_ass4 : forall l1 l2 l3 l4 : natlist,
+	l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
+Proof.
+	intros l1 l2 l3 l4.
+	rewrite -> app_ass.
+	rewrite -> app_ass.
+	reflexivity.
+	Qed.
+
+Theorem snoc_append : forall (l : natlist) (n : nat),
+	snoc l n = l ++ [n].
+Proof.
+	intros l n.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite -> IHl.
+		reflexivity.
+		Qed.
+
+Theorem nonzeros_length : forall l1 l2 : natlist,
+	nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
+Proof.
+	intros l1 l2.
+	induction l1.
+	Case "l1 = nil".
+		reflexivity.
+	Case "l1 = cons".
+		simpl.
+		rewrite -> IHl1.
+		destruct n.
+		reflexivity.
+		reflexivity.
+		Qed.
+
+Theorem distr_rev : forall l1 l2 : natlist,
+	rev (l1 ++ l2) = (rev l2) ++ (rev l1).
+Proof.
+	intros l1 l2.
+	induction l1.
+	Case "l1 = nil".
+		simpl.
+		rewrite -> app_nil_end.
+		reflexivity.
+	Case "l1 = cons".
+		simpl.
+		rewrite -> IHl1.
+		simpl.
+		rewrite -> snoc_append.
+		rewrite -> snoc_append.
+		rewrite -> app_ass.
+		reflexivity.
+		Qed.
+
+Theorem count_number_nonzero : forall (s : bag),
+	ble_nat O (count (S O) (S O :: s)) = true.
+Proof.
+	intros s.
+	induction s.
+		reflexivity.
+		reflexivity.
+		Qed.
+
+Theorem ble_n_Sn : forall n,
+	ble_nat n (S n) = true.
+Proof.
+	intros n. induction n as [| n'].
+	Case "0".
+		simpl. reflexivity.
+	Case "S n'".
+		simpl. rewrite -> IHn'. reflexivity. Qed.
+
+Theorem remove_decreases_count: forall (s : bag),
+	ble_nat (count O (remove_one O s)) (count O s) = true.
+Proof.
+	intros s.
+	induction s.
+	Case "s = nil".
+		reflexivity.
+	Case "s = cons".
+		simpl.
+		induction n.
+		SCase "n = O".
+			simpl.  rewrite -> ble_n_Sn.
+			reflexivity.
+		SCase "n = S n'".
+			simpl.
+			rewrite -> IHs.
+			reflexivity.
+			Qed.
+
+Inductive natoption : Type :=
+	| Some : nat -> natoption
+	| None : natoption.
+
+Fixpoint index (n:nat) (l:natlist) : natoption :=
+	match l with
+		| nil => None
+		| a :: l' => if beq_nat n O then Some a else index (pred n) l'
+  end.
+
+Definition option_elim (o : natoption) (d : nat) : nat :=
+	match o with
+		| Some n' => n'
+		| None => d
+	end.
+
+Definition hd_opt (l : natlist) : natoption :=
+	match l with
+		| nil => None
+		| v :: r => Some v
+	end.
+
+Example test_hd_opt1 : hd_opt [] = None.
+Proof. reflexivity. Qed.
+Example test_hd_opt2 : hd_opt [S O] = Some (S O).
+Proof. reflexivity. Qed.
+
+Theorem option_elim_hd : forall l:natlist,
+	head l = option_elim (hd_opt l) O.
+Proof.
+	intros l.
+	destruct l.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
+	match l1 with
+		| nil => match l2 with
+							| nil => true
+							| _ => false
+						 end
+		| v1 :: r1 => match l2 with
+									 | nil => false
+									 | v2 :: r2 => if beq_nat v1 v2 then beq_natlist r1 r2
+																 else false
+									end
+	end.
+
+Example test_beq_natlist1 : (beq_natlist nil nil = true).
+Proof. reflexivity. Qed.
+Example test_beq_natlist2 : (beq_natlist [S O, S (S O), S (S (S O))]
+																				 [S O, S (S O), S (S (S O))] = true).
+Proof. reflexivity. Qed.
+
+Theorem beq_natlist_refl : forall l:natlist,
+	beq_natlist l l = true.
+Proof.
+	intros l.
+	induction l.
+	Case "l = nil".
+		reflexivity.
+	Case "l = cons".
+		simpl.
+		rewrite <- beq_nat_refl.
+		rewrite -> IHl.
+		reflexivity.
+	Qed.
+
+Theorem silly1 : forall (n m o p : nat),
+	n = m -> [n, o] = [n, p] -> [n, o] = [m, p].
+Proof.
+	intros n m o p eq1 eq2.
+	rewrite <- eq1.
+	apply eq2. Qed.
+
+Theorem silly2a : forall (n m : nat),
+	(n,n) = (m,m) ->
+		(forall (q r : nat), (q, q) = (r, r) -> [q] = [r]) ->
+			[n] = [m].
+Proof.
+	intros n m eq1 eq2.
+	apply eq2.
+	apply eq1.
+	Qed.
+
+Theorem silly_ex :
+	(forall n, evenb n = true -> oddb (S n) = true) ->
+	evenb (S (S (S O))) = true ->
+	oddb (S (S (S (S O)))) = true.
+Proof.
+	intros eq1 eq2.
+	apply eq1.
+	apply eq2.
+	Qed.
+
+Theorem silly3 : forall (n : nat),
+	true = beq_nat n (S (S (S (S (S O))))) ->
+	beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))) = true.
+Proof.
+	intros n H.
+	symmetry.
+	apply H.
+	Qed.
+
+Theorem rev_exercise : forall (l l' : natlist),
+	l = rev l' -> l' = rev l.
+Proof.
+	intros l l' H.
+	rewrite -> H.
+	rewrite -> rev_involutive.
+	reflexivity.
+	Qed.
+
+Theorem beq_nat_sym : forall (n m:nat), forall (b: bool),
+	beq_nat n m = b -> beq_nat m n = b.
+Proof.
+	intros n.
+	induction n as [| n'].
+	Case "n = O".
+		intros m b eq1.
+		induction m.
+		SCase "m = 0".
+			apply eq1.
+		SCase "m = S m'".
+			apply eq1.
+	Case "n = S n'".
+		induction m.
+		SCase "m = 0".
+			intros b eq1.
+			apply eq1.
+		SCase "m = S m'".
+			intros b eq1.
+			apply IHn'.
+			apply eq1.
+		Qed.
+
+Theorem app_ass' : forall l1 l2 l3 : natlist,
+	(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+Proof.
+	intros l1. induction l1 as [ | n l1'].
+	reflexivity.
+	simpl.
+	intros l2 l3.
+	rewrite -> IHl1'.
+	reflexivity.
+	Qed.
+
+End NatList.

samples/Coq/PermutSetoid.v

@@ -0,0 +1,547 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Omega Relations Multiset SetoidList.
+
+(** This file is deprecated, use [Permutation.v] instead.
+
+    Indeed, this file defines a notion of permutation based on
+    multisets (there exists a permutation between two lists iff every
+    elements have the same multiplicity in the two lists) which
+    requires a more complex apparatus (the equipment of the domain
+    with a decidable equality) than [Permutation] in [Permutation.v].
+
+    The relation between the two relations are in lemma
+    [permutation_Permutation].
+
+    File [Permutation] concerns Leibniz equality : it shows in particular
+    that [List.Permutation] and [permutation] are equivalent in this context.
+*)
+
+Set Implicit Arguments.
+
+Local Notation "[ ]" := nil.
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
+
+Section Permut.
+
+(** * From lists to multisets *)
+
+Variable A : Type.
+Variable eqA : relation A.
+Hypothesis eqA_equiv : Equivalence eqA.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
+
+(** contents of a list *)
+
+Fixpoint list_contents (l:list A) : multiset A :=
+  match l with
+  | [] => emptyBag
+  | a :: l => munion (singletonBag a) (list_contents l)
+  end.
+
+Lemma list_contents_app :
+  forall l m:list A,
+    meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
+Proof.
+  simple induction l; simpl; auto with datatypes.
+  intros.
+  apply meq_trans with
+    (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
+    auto with datatypes.
+Qed.
+
+(** * [permutation]: definition and basic properties *)
+
+Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).
+
+Lemma permut_refl : forall l:list A, permutation l l.
+Proof.
+  unfold permutation; auto with datatypes.
+Qed.
+
+Lemma permut_sym :
+  forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
+Proof.
+  unfold permutation, meq; intros; symmetry; trivial.
+Qed.
+
+Lemma permut_trans :
+  forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
+Proof.
+  unfold permutation; intros.
+  apply meq_trans with (list_contents m); auto with datatypes.
+Qed.
+
+Lemma permut_cons_eq :
+  forall l m:list A,
+    permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).
+Proof.
+  unfold permutation; simpl; intros.
+  apply meq_trans with (munion (singletonBag a') (list_contents l)).
+  apply meq_left, meq_singleton; auto.
+  auto with datatypes.
+Qed.
+
+Lemma permut_cons :
+  forall l m:list A,
+    permutation l m -> forall a:A, permutation (a :: l) (a :: m).
+Proof.
+  unfold permutation; simpl; auto with datatypes.
+Qed.
+
+Lemma permut_app :
+  forall l l' m m':list A,
+    permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
+Proof.
+  unfold permutation; intros.
+  apply meq_trans with (munion (list_contents l) (list_contents m));
+    auto using permut_cons, list_contents_app with datatypes.
+  apply meq_trans with (munion (list_contents l') (list_contents m'));
+    auto using permut_cons, list_contents_app with datatypes.
+  apply meq_trans with (munion (list_contents l') (list_contents m));
+    auto using permut_cons, list_contents_app with datatypes.
+Qed.
+
+Lemma permut_add_inside_eq :
+  forall a a' l1 l2 l3 l4, eqA a a' ->
+    permutation (l1 ++ l2) (l3 ++ l4) ->
+    permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).
+Proof.
+  unfold permutation, meq in *; intros.
+  specialize H0 with a0.
+  repeat rewrite list_contents_app in *; simpl in *.
+  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha;
+    decide (eqA_dec a' a0) with Ha; simpl; auto with arith.
+  do 2 rewrite <- plus_n_Sm; f_equal; auto.
+Qed.
+
+Lemma permut_add_inside :
+  forall a l1 l2 l3 l4,
+    permutation (l1 ++ l2) (l3 ++ l4) ->
+    permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
+Proof.
+  unfold permutation, meq in *; intros.
+  generalize (H a0); clear H.
+  do 4 rewrite list_contents_app.
+  simpl.
+  destruct (eqA_dec a a0); simpl; auto with arith.
+  do 2 rewrite <- plus_n_Sm; f_equal; auto.
+Qed.
+
+Lemma permut_add_cons_inside_eq :
+  forall a a' l l1 l2, eqA a a' ->
+    permutation l (l1 ++ l2) ->
+    permutation (a :: l) (l1 ++ a' :: l2).
+Proof.
+  intros;
+  replace (a :: l) with ([] ++ a :: l); trivial;
+    apply permut_add_inside_eq; trivial.
+Qed.
+
+Lemma permut_add_cons_inside :
+  forall a l l1 l2,
+    permutation l (l1 ++ l2) ->
+    permutation (a :: l) (l1 ++ a :: l2).
+Proof.
+  intros;
+    replace (a :: l) with ([] ++ a :: l); trivial;
+	apply permut_add_inside; trivial.
+Qed.
+
+Lemma permut_middle :
+  forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
+Proof.
+  intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
+Qed.
+
+Lemma permut_sym_app :
+  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
+Proof.
+  intros l1 l2;
+    unfold permutation, meq;
+	intro a; do 2 rewrite list_contents_app; simpl;
+	  auto with arith.
+Qed.
+
+Lemma permut_rev :
+  forall l, permutation l (rev l).
+Proof.
+  induction l.
+  simpl; trivial using permut_refl.
+  simpl.
+  apply permut_add_cons_inside.
+  rewrite <- app_nil_end. trivial.
+Qed.
+
+(** * Some inversion results. *)
+Lemma permut_conv_inv :
+  forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
+Proof.
+  intros e l1 l2; unfold permutation, meq; simpl; intros H a;
+    generalize (H a); apply plus_reg_l.
+Qed.
+
+Lemma permut_app_inv1 :
+  forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
+Proof.
+  intros l l1 l2; unfold permutation, meq; simpl;
+    intros H a; generalize (H a); clear H.
+  do 2 rewrite list_contents_app.
+  simpl.
+  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
+  rewrite plus_comm; rewrite H; rewrite plus_comm.
+  trivial.
+Qed.
+
+(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
+
+Fact if_eqA_then : forall a a' (B:Type)(b b':B),
+ eqA a a' -> (if eqA_dec a a' then b else b') = b.
+Proof.
+  intros. destruct eqA_dec as [_|NEQ]; auto.
+  contradict NEQ; auto.
+Qed.
+
+Lemma permut_app_inv2 :
+  forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
+Proof.
+  intros l l1 l2; unfold permutation, meq; simpl;
+    intros H a; generalize (H a); clear H.
+  do 2 rewrite list_contents_app.
+  simpl.
+  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
+  trivial.
+Qed.
+
+Lemma permut_remove_hd_eq :
+  forall l l1 l2 a b, eqA a b ->
+    permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).
+Proof.
+  unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.
+  specialize H with a0.
+  rewrite list_contents_app in *; simpl in *.
+  apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
+  rewrite H; clear H.
+  symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal.
+  rewrite plus_comm.
+  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha;
+    decide (eqA_dec b a0) with Ha; reflexivity.
+Qed.
+
+Lemma permut_remove_hd :
+  forall l l1 l2 a,
+    permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
+Proof.
+  eauto using permut_remove_hd_eq, Equivalence_Reflexive.
+Qed.
+
+Fact if_eqA_else : forall a a' (B:Type)(b b':B),
+ ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
+Proof.
+  intros. decide (eqA_dec a a') with H; auto.
+Qed.
+
+Fact if_eqA_refl : forall a (B:Type)(b b':B),
+ (if eqA_dec a a then b else b') = b.
+Proof.
+  intros; apply (decide_left (eqA_dec a a)); auto with *.
+Qed.
+
+(** PL: Inutilisable dans un rewrite sans un change prealable. *)
+
+Global Instance if_eqA (B:Type)(b b':B) :
+ Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
+Proof.
+ intros x x' Hxx' y y' Hyy'.
+ intros; destruct (eqA_dec x y) as [H|H];
+  destruct (eqA_dec x' y') as [H'|H']; auto.
+ contradict H'; transitivity x; auto with *; transitivity y; auto with *.
+ contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
+Qed.
+
+Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
+ eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
+               (if eqA_dec a1' a2 then b else b').
+Proof.
+ intros; destruct (eqA_dec a1 a2) as [A1|A1];
+  destruct (eqA_dec a1' a2) as [A1'|A1']; auto.
+ contradict A1'; transitivity a1; eauto with *.
+ contradict A1; transitivity a1'; eauto with *.
+Qed.
+
+Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
+ eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
+               (if eqA_dec a1 a2' then b else b').
+Proof.
+ intros; destruct (eqA_dec a1 a2) as [A2|A2];
+  destruct (eqA_dec a1 a2') as [A2'|A2']; auto.
+ contradict A2'; transitivity a2; eauto with *.
+ contradict A2; transitivity a2'; eauto with *.
+Qed.
+
+
+Global Instance multiplicity_eqA (l:list A) :
+ Proper (eqA==>@eq _) (multiplicity (list_contents l)).
+Proof.
+  intros x x' Hxx'.
+  induction l as [|y l Hl]; simpl; auto.
+  rewrite (@if_eqA_rewrite_r y x x'); auto.
+Qed.
+
+Lemma multiplicity_InA :
+  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
+Proof.
+  induction l.
+  simpl.
+  split; inversion 1.
+  simpl.
+  intros a'; split; intros H. inversion_clear H.
+  apply (decide_left (eqA_dec a a')); auto with *.
+  destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto.
+  destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto.
+Qed.
+
+Lemma multiplicity_InA_O :
+  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
+Proof.
+  intros l a; rewrite multiplicity_InA;
+    destruct (multiplicity (list_contents l) a); auto with arith.
+  destruct 1; auto with arith.
+Qed.
+
+Lemma multiplicity_InA_S :
+  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
+Proof.
+  intros l a; rewrite multiplicity_InA; auto with arith.
+Qed.
+
+Lemma multiplicity_NoDupA : forall l,
+  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
+Proof.
+  induction l.
+  simpl.
+  split; auto with arith.
+  split; simpl.
+  inversion_clear 1.
+  rewrite IHl in H1.
+  intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.
+  rewrite <- EQ.
+  rewrite multiplicity_InA_O; auto.
+  intros; constructor.
+  rewrite multiplicity_InA.
+  specialize (H a).
+  rewrite if_eqA_refl in H.
+  clear IHl; omega.
+  rewrite IHl; intros.
+  specialize (H a0). omega.
+Qed.
+
+(** Permutation is compatible with InA. *)
+Lemma permut_InA_InA :
+  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
+Proof.
+  intros l1 l2 e.
+  do 2 rewrite multiplicity_InA.
+  unfold permutation, meq.
+  intros H;rewrite H; auto.
+Qed.
+
+Lemma permut_cons_InA :
+  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
+Proof.
+  intros; apply (permut_InA_InA (e:=e) H); auto with *.
+Qed.
+
+(** Permutation of an empty list. *)
+Lemma permut_nil :
+  forall l, permutation l [] -> l = [].
+Proof.
+  intro l; destruct l as [ | e l ]; trivial.
+  assert (InA eqA e (e::l)) by (auto with *).
+  intro Abs; generalize (permut_InA_InA Abs H).
+  inversion 1.
+Qed.
+
+(** Permutation for short lists. *)
+
+Lemma permut_length_1:
+  forall a b, permutation [a] [b] -> eqA a b.
+Proof.
+  intros a b; unfold permutation, meq.
+  intro P; specialize (P b); simpl in *.
+  rewrite if_eqA_refl in *.
+  destruct (eqA_dec a b); simpl; auto; discriminate.
+Qed.
+
+Lemma permut_length_2 :
+  forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
+    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
+Proof.
+  intros a1 b1 a2 b2 P.
+  assert (H:=permut_cons_InA P).
+  inversion_clear H.
+  left; split; auto.
+  apply permut_length_1.
+  red; red; intros.
+  specialize (P a). simpl in *.
+  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega.
+  right.
+  inversion_clear H0; [|inversion H].
+  split; auto.
+  apply permut_length_1.
+  red; red; intros.
+  specialize (P a); simpl in *.
+  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega.
+Qed.
+
+(** Permutation is compatible with length. *)
+Lemma permut_length :
+  forall l1 l2, permutation l1 l2 -> length l1 = length l2.
+Proof.
+  induction l1; intros l2 H.
+  rewrite (permut_nil (permut_sym H)); auto.
+  assert (H0:=permut_cons_InA H).
+  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+  subst l2.
+  rewrite app_length.
+  simpl; rewrite <- plus_n_Sm; f_equal.
+  rewrite <- app_length.
+  apply IHl1.
+  apply permut_remove_hd with b.
+  apply permut_trans with (a::l1); auto.
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  rewrite (@if_eqA_rewrite_l a b a0); auto.
+Qed.
+
+Lemma NoDupA_equivlistA_permut :
+  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
+    equivlistA eqA l l' -> permutation l l'.
+Proof.
+  intros.
+  red; unfold meq; intros.
+  rewrite multiplicity_NoDupA in H, H0.
+  generalize (H a) (H0 a) (H1 a); clear H H0 H1.
+  do 2 rewrite multiplicity_InA.
+  destruct 3; omega.
+Qed.
+
+End Permut.
+
+Section Permut_map.
+
+Variables A B : Type.
+
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis eqA_equiv : Equivalence eqA.
+
+Variable eqB : B->B->Prop.
+Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
+Hypothesis eqB_trans : Transitive eqB.
+
+(** Permutation is compatible with map. *)
+
+Lemma permut_map :
+  forall f,
+    (Proper (eqA==>eqB) f) ->
+    forall l1 l2, permutation _ eqA_dec l1 l2 ->
+      permutation _ eqB_dec (map f l1) (map f l2).
+Proof.
+  intros f; induction l1.
+  intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl.
+  intros l2 P.
+  simpl.
+  assert (H0:=permut_cons_InA eqA_equiv P).
+  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+  subst l2.
+  rewrite map_app.
+  simpl.
+  apply permut_trans with (f b :: map f l1).
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  destruct (eqB_dec (f b) a0) as [H2|H2];
+    destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
+  destruct H3; transitivity (f b); auto with *.
+  destruct H2; transitivity (f a); auto with *.
+  apply permut_add_cons_inside.
+  rewrite <- map_app.
+  apply IHl1; auto.
+  apply permut_remove_hd with b; trivial.
+  apply permut_trans with (a::l1); auto.
+  revert H1; unfold permutation, meq; simpl.
+  intros; f_equal; auto.
+  rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto.
+Qed.
+
+End Permut_map.
+
+Require Import Permutation.
+
+Section Permut_permut.
+
+Variable A : Type.
+
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis eqA_equiv : Equivalence eqA.
+
+Lemma Permutation_impl_permutation : forall l l',
+  Permutation l l' -> permutation _ eqA_dec l l'.
+Proof.
+  induction 1.
+    apply permut_refl.
+    apply permut_cons; auto using Equivalence_Reflexive.
+    change (x :: y :: l) with ([x] ++ y :: l);
+      apply permut_add_cons_inside; simpl;
+      apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl.
+    apply permut_trans with l'; trivial.
+Qed.
+
+Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.
+Proof.
+  induction 1.
+    apply permut_refl.
+    apply permut_cons_eq; trivial.
+Qed.
+
+Lemma permutation_Permutation : forall l l',
+  permutation _ eqA_dec l l' <->
+  exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.
+Proof.
+  split; intro H.
+  (* -> *)
+  induction l in l', H |- *.
+    exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2.
+    pose proof H as H'.
+    apply permut_cons_InA, InA_split in H
+      as (l1 & y & l2 & Heq & ->); trivial.
+    apply permut_remove_hd_eq, IHl in H'
+      as (l'' & IHP & IHA); clear IHl; trivial.
+    apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->).
+    exists (l1'' ++ a :: l2''); split.
+      apply Permutation_cons_app; trivial.
+      apply Forall2_app, Forall2_cons; trivial.
+  (* <- *)
+  destruct H as (l'' & H & Heq).
+  apply permut_trans with l''.
+    apply Permutation_impl_permutation; trivial.
+    apply permut_eqA; trivial.
+Qed.
+
+End Permut_permut.
+
+(* begin hide *)
+(** For compatibilty *)
+Notation permut_right := permut_cons (only parsing).
+Notation permut_tran := permut_trans (only parsing).
+(* end hide *)

samples/Coq/Permutation.v

@@ -0,0 +1,644 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*********************************************************************)
+(** * List permutations as a composition of adjacent transpositions  *)
+(*********************************************************************)
+
+(* Adapted in May 2006 by Jean-Marc Notin from initial contents by
+   Laurent Théry (Huffmann contribution, October 2003) *)
+
+Require Import List Setoid Compare_dec Morphisms.
+Import ListNotations. (* For notations [] and [a;b;c] *)
+Set Implicit Arguments.
+
+Section Permutation.
+
+Variable A:Type.
+
+Inductive Permutation : list A -> list A -> Prop :=
+| perm_nil: Permutation [] []
+| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
+| perm_swap x y l : Permutation (y::x::l) (x::y::l)
+| perm_trans l l' l'' :
+    Permutation l l' -> Permutation l' l'' -> Permutation l l''.
+
+Local Hint Constructors Permutation.
+
+(** Some facts about [Permutation] *)
+
+Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].
+Proof.
+  intros l HF.
+  remember (@nil A) as m in HF.
+  induction HF; discriminate || auto.
+Qed.
+
+Theorem Permutation_nil_cons : forall (l : list A) (x : A),
+ ~ Permutation nil (x::l).
+Proof.
+  intros l x HF.
+  apply Permutation_nil in HF; discriminate.
+Qed.
+
+(** Permutation over lists is a equivalence relation *)
+
+Theorem Permutation_refl : forall l : list A, Permutation l l.
+Proof.
+  induction l; constructor. exact IHl.
+Qed.
+
+Theorem Permutation_sym : forall l l' : list A,
+ Permutation l l' -> Permutation l' l.
+Proof.
+  intros l l' Hperm; induction Hperm; auto.
+  apply perm_trans with (l':=l'); assumption.
+Qed.
+
+Theorem Permutation_trans : forall l l' l'' : list A,
+ Permutation l l' -> Permutation l' l'' -> Permutation l l''.
+Proof.
+  exact perm_trans.
+Qed.
+
+End Permutation.
+
+Hint Resolve Permutation_refl perm_nil perm_skip.
+
+(* These hints do not reduce the size of the problem to solve and they
+   must be used with care to avoid combinatoric explosions *)
+
+Local Hint Resolve perm_swap perm_trans.
+Local Hint Resolve Permutation_sym Permutation_trans.
+
+(* This provides reflexivity, symmetry and transitivity and rewriting
+   on morphims to come *)
+
+Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
+  Equivalence_Reflexive := @Permutation_refl A ;
+  Equivalence_Symmetric := @Permutation_sym A ;
+  Equivalence_Transitive := @Permutation_trans A }.
+
+Instance Permutation_cons A :
+ Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.
+Proof.
+  repeat intro; subst; auto using perm_skip.
+Qed.
+
+Section Permutation_properties.
+
+Variable A:Type.
+
+Implicit Types a b : A.
+Implicit Types l m : list A.
+
+(** Compatibility with others operations on lists *)
+
+Theorem Permutation_in : forall (l l' : list A) (x : A),
+ Permutation l l' -> In x l -> In x l'.
+Proof.
+  intros l l' x Hperm; induction Hperm; simpl; tauto.
+Qed.
+
+Global Instance Permutation_in' :
+ Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10.
+Proof.
+  repeat red; intros; subst; eauto using Permutation_in.
+Qed.
+
+Lemma Permutation_app_tail : forall (l l' tl : list A),
+ Permutation l l' -> Permutation (l++tl) (l'++tl).
+Proof.
+  intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.
+  eapply Permutation_trans with (l':=l'++tl); trivial.
+Qed.
+
+Lemma Permutation_app_head : forall (l tl tl' : list A),
+ Permutation tl tl' -> Permutation (l++tl) (l++tl').
+Proof.
+  intros l tl tl' Hperm; induction l;
+   [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
+Qed.
+
+Theorem Permutation_app : forall (l m l' m' : list A),
+ Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
+Proof.
+  intros l m l' m' Hpermll' Hpermmm';
+   induction Hpermll' as [|x l l'|x y l|l l' l''];
+    repeat rewrite <- app_comm_cons; auto.
+  apply Permutation_trans with (l' := (x :: y :: l ++ m));
+   [idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.
+  apply Permutation_trans with (l' := (l' ++ m')); try assumption.
+  apply Permutation_app_tail; assumption.
+Qed.
+
+Global Instance Permutation_app' :
+ Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10.
+Proof.
+  repeat intro; now apply Permutation_app.
+Qed.
+
+Lemma Permutation_add_inside : forall a (l l' tl tl' : list A),
+  Permutation l l' -> Permutation tl tl' ->
+  Permutation (l ++ a :: tl) (l' ++ a :: tl').
+Proof.
+  intros; apply Permutation_app; auto.
+Qed.
+
+Lemma Permutation_cons_append : forall (l : list A) x,
+  Permutation (x :: l) (l ++ x :: nil).
+Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed.
+Local Hint Resolve Permutation_cons_append.
+
+Theorem Permutation_app_comm : forall (l l' : list A),
+  Permutation (l ++ l') (l' ++ l).
+Proof.
+  induction l as [|x l]; simpl; intro l'.
+  rewrite app_nil_r; trivial. rewrite IHl.
+  rewrite app_comm_cons, Permutation_cons_append.
+  now rewrite <- app_assoc.
+Qed.
+Local Hint Resolve Permutation_app_comm.
+
+Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
+  Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
+Proof.
+  intros l l1 l2 a H. rewrite H.
+  rewrite app_comm_cons, Permutation_cons_append.
+  now rewrite <- app_assoc.
+Qed.
+Local Hint Resolve Permutation_cons_app.
+
+Theorem Permutation_middle : forall (l1 l2:list A) a,
+  Permutation (a :: l1 ++ l2) (l1 ++ a :: l2).
+Proof.
+  auto.
+Qed.
+Local Hint Resolve Permutation_middle.
+
+Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
+Proof.
+  induction l as [| x l]; simpl; trivial. now rewrite IHl at 1.
+Qed.
+
+Global Instance Permutation_rev' :
+ Proper (@Permutation A ==> @Permutation A) (@rev A) | 10.
+Proof.
+  repeat intro; now rewrite <- 2 Permutation_rev.
+Qed.
+
+Theorem Permutation_length : forall (l l' : list A),
+ Permutation l l' -> length l = length l'.
+Proof.
+  intros l l' Hperm; induction Hperm; simpl; auto. now transitivity (length l').
+Qed.
+
+Global Instance Permutation_length' :
+ Proper (@Permutation A ==> Logic.eq) (@length A) | 10.
+Proof.
+  exact Permutation_length.
+Qed.
+
+Theorem Permutation_ind_bis :
+ forall P : list A -> list A -> Prop,
+   P [] [] ->
+   (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
+   (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
+   (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
+   forall l l', Permutation l l' -> P l l'.
+Proof.
+  intros P Hnil Hskip Hswap Htrans.
+  induction 1; auto.
+  apply Htrans with (x::y::l); auto.
+  apply Hswap; auto.
+  induction l; auto.
+  apply Hskip; auto.
+  apply Hskip; auto.
+  induction l; auto.
+  eauto.
+Qed.
+
+Ltac break_list l x l' H :=
+  destruct l as [|x l']; simpl in *;
+  injection H; intros; subst; clear H.
+
+Theorem Permutation_nil_app_cons : forall (l l' : list A) (x : A),
+ ~ Permutation nil (l++x::l').
+Proof.
+  intros l l' x HF.
+  apply Permutation_nil in HF. destruct l; discriminate.
+Qed.
+
+Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
+  Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
+Proof.
+  intros l1 l2 l3 l4 a; revert l1 l2 l3 l4.
+  set (P l l' :=
+       forall l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 ->
+       Permutation (l1++l2) (l3++l4)).
+  cut (forall l l', Permutation l l' -> P l l').
+  intros H; intros; eapply H; eauto.
+  apply (Permutation_ind_bis P); unfold P; clear P.
+  - (* nil *)
+    intros; now destruct l1.
+  - (* skip *)
+    intros x l l' H IH; intros.
+    break_list l1 b l1' H0; break_list l3 c l3' H1.
+    auto.
+    now rewrite H.
+    now rewrite <- H.
+    now rewrite (IH _ _ _ _ eq_refl eq_refl).
+  - (* swap *)
+    intros x y l l' Hp IH; intros.
+    break_list l1 b l1' H; break_list l3 c l3' H0.
+    auto.
+    break_list l3' b l3'' H.
+    auto.
+    constructor. now rewrite Permutation_middle.
+    break_list l1' c l1'' H1.
+    auto.
+    constructor. now rewrite Permutation_middle.
+    break_list l3' d l3'' H; break_list l1' e l1'' H1.
+    auto.
+    rewrite perm_swap. constructor. now rewrite Permutation_middle.
+    rewrite perm_swap. constructor. now rewrite Permutation_middle.
+    now rewrite perm_swap, (IH _ _ _ _ eq_refl eq_refl).
+  - (*trans*)
+    intros.
+    destruct (In_split a l') as (l'1,(l'2,H6)).
+    rewrite <- H.
+    subst l.
+    apply in_or_app; right; red; auto.
+    apply perm_trans with (l'1++l'2).
+    apply (H0 _ _ _ _ H3 H6).
+    apply (H2 _ _ _ _ H6 H4).
+Qed.
+
+Theorem Permutation_cons_inv l l' a :
+ Permutation (a::l) (a::l') -> Permutation l l'.
+Proof.
+  intro H; exact (Permutation_app_inv [] l [] l' a H).
+Qed.
+
+Theorem Permutation_cons_app_inv l l1 l2 a :
+ Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
+Proof.
+  intro H; exact (Permutation_app_inv [] l l1 l2 a H).
+Qed.
+
+Theorem Permutation_app_inv_l : forall l l1 l2,
+ Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
+Proof.
+  induction l; simpl; auto.
+  intros.
+  apply IHl.
+  apply Permutation_cons_inv with a; auto.
+Qed.
+
+Theorem Permutation_app_inv_r : forall l l1 l2,
+ Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
+Proof.
+  induction l.
+  intros l1 l2; do 2 rewrite app_nil_r; auto.
+  intros.
+  apply IHl.
+  apply Permutation_app_inv with a; auto.
+Qed.
+
+Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
+Proof.
+  intros a l H; remember [a] as m in H.
+  induction H; try (injection Heqm as -> ->; clear Heqm);
+    discriminate || auto.
+  apply Permutation_nil in H as ->; trivial.
+Qed.
+
+Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.
+Proof.
+  intros a b H.
+  apply Permutation_length_1_inv in H; injection H as ->; trivial.
+Qed.
+
+Lemma Permutation_length_2_inv :
+  forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1].
+Proof.
+  intros a1 a2 l H; remember [a1;a2] as m in H.
+  revert a1 a2 Heqm.
+  induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
+    discriminate || (try tauto).
+  apply Permutation_length_1_inv in H as ->; left; auto.
+  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as ();
+    auto.
+Qed.
+
+Lemma Permutation_length_2 :
+  forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] ->
+    a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
+Proof.
+  intros a1 b1 a2 b2 H.
+  apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto.
+Qed.
+
+Let in_middle l l1 l2 (a:A) : l = l1 ++ a :: l2 ->
+ forall x, In x l <-> a = x \/ In x (l1++l2).
+Proof.
+ intros; subst; rewrite !in_app_iff; simpl. tauto.
+Qed.
+
+Lemma NoDup_cardinal_incl (l l' : list A) : NoDup l -> NoDup l' ->
+  length l = length l' -> incl l l' -> incl l' l.
+Proof.
+ intros N. revert l'. induction N as [|a l Hal Hl IH].
+ - destruct l'; now auto.
+ - intros l' Hl' E H x Hx.
+   assert (Ha : In a l') by (apply H; simpl; auto).
+   destruct (in_split _ _ Ha) as (l1 & l2 & H12). clear Ha.
+   rewrite in_middle in Hx; eauto.
+   destruct Hx as [Hx|Hx]; [left|right]; auto.
+   apply (IH (l1++l2)); auto.
+   * apply NoDup_remove_1 with a; rewrite <- H12; auto.
+   * apply eq_add_S.
+     simpl in E; rewrite E, H12, !app_length; simpl; auto with arith.
+   * intros y Hy. assert (Hy' : In y l') by (apply H; simpl; auto).
+     rewrite in_middle in Hy'; eauto.
+     destruct Hy'; auto. subst y; intuition.
+Qed.
+
+Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' ->
+  (forall x:A, In x l <-> In x l') -> Permutation l l'.
+Proof.
+ intros N. revert l'. induction N as [|a l Hal Hl IH].
+ - destruct l'; simpl; auto.
+   intros Hl' H. exfalso. rewrite (H a); auto.
+ - intros l' Hl' H.
+   assert (Ha : In a l') by (apply H; simpl; auto).
+   destruct (In_split _ _ Ha) as (l1 & l2 & H12).
+   rewrite H12.
+   apply Permutation_cons_app.
+   apply IH; auto.
+   * apply NoDup_remove_1 with a; rewrite <- H12; auto.
+   * intro x. split; intros Hx.
+     + assert (Hx' : In x l') by (apply H; simpl; auto).
+       rewrite in_middle in Hx'; eauto.
+       destruct Hx'; auto. subst; intuition.
+     + assert (Hx' : In x l') by (rewrite (in_middle l1 l2 a); eauto).
+       rewrite <- H in Hx'. destruct Hx'; auto.
+       subst. destruct (NoDup_remove_2 _ _ _ Hl' Hx).
+Qed.
+
+Lemma NoDup_Permutation_bis l l' : NoDup l -> NoDup l' ->
+  length l = length l' -> incl l l' -> Permutation l l'.
+Proof.
+ intros. apply NoDup_Permutation; auto.
+ split; auto. apply NoDup_cardinal_incl; auto.
+Qed.
+
+Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'.
+Proof.
+ induction 1; auto.
+ * inversion_clear 1; constructor; eauto using Permutation_in.
+ * inversion_clear 1 as [|? ? H1 H2]. inversion_clear H2; simpl in *.
+   constructor. simpl; intuition. constructor; intuition.
+Qed.
+
+Global Instance Permutation_NoDup' :
+ Proper (@Permutation A ==> iff) (@NoDup A) | 10.
+Proof.
+  repeat red; eauto using Permutation_NoDup.
+Qed.
+
+End Permutation_properties.
+
+Section Permutation_map.
+
+Variable A B : Type.
+Variable f : A -> B.
+
+Lemma Permutation_map l l' :
+  Permutation l l' -> Permutation (map f l) (map f l').
+Proof.
+ induction 1; simpl; eauto.
+Qed.
+
+Global Instance Permutation_map' :
+  Proper (@Permutation A ==> @Permutation B) (map f) | 10.
+Proof.
+  exact Permutation_map.
+Qed.
+
+End Permutation_map.
+
+Section Injection.
+
+Definition injective {A B} (f : A->B) :=
+ forall x y, f x = f y -> x = y.
+
+Lemma injective_map_NoDup {A B} (f:A->B) (l:list A) :
+ injective f -> NoDup l -> NoDup (map f l).
+Proof.
+ intros Hf. induction 1 as [|x l Hx Hl IH]; simpl; constructor; trivial.
+ rewrite in_map_iff. intros (y & Hy & Hy'). apply Hf in Hy. now subst.
+Qed.
+
+Lemma injective_bounded_surjective n f :
+ injective f ->
+ (forall x, x < n -> f x < n) ->
+ (forall y, y < n -> exists x, x < n /\ f x = y).
+Proof.
+ intros Hf H.
+ set (l := seq 0 n).
+ assert (P : incl (map f l) l).
+ { intros x. rewrite in_map_iff. intros (y & <- & Hy').
+   unfold l in *. rewrite in_seq in *. simpl in *.
+   destruct Hy' as (_,Hy'). auto with arith. }
+ assert (P' : incl l (map f l)).
+ { unfold l.
+   apply NoDup_cardinal_incl; auto using injective_map_NoDup, seq_NoDup.
+   now rewrite map_length. }
+ intros x Hx.
+ assert (Hx' : In x l) by (unfold l; rewrite in_seq; auto with arith).
+ apply P' in Hx'.
+ rewrite in_map_iff in Hx'. destruct Hx' as (y & Hy & Hy').
+ exists y; split; auto. unfold l in *; rewrite in_seq in Hy'.
+ destruct Hy'; auto with arith.
+Qed.
+
+Lemma nat_bijection_Permutation n f :
+ injective f -> (forall x, x < n -> f x < n) ->
+ let l := seq 0 n in Permutation (map f l) l.
+Proof.
+ intros Hf BD.
+ apply NoDup_Permutation_bis; auto using injective_map_NoDup, seq_NoDup.
+ * now rewrite map_length.
+ * intros x. rewrite in_map_iff. intros (y & <- & Hy').
+   rewrite in_seq in *. simpl in *.
+   destruct Hy' as (_,Hy'). auto with arith.
+Qed.
+
+End Injection.
+
+Section Permutation_alt.
+Variable A:Type.
+Implicit Type a : A.
+Implicit Type l : list A.
+
+(** Alternative characterization of permutation
+    via [nth_error] and [nth] *)
+
+Let adapt f n :=
+ let m := f (S n) in if le_lt_dec m (f 0) then m else pred m.
+
+Let adapt_injective f : injective f -> injective (adapt f).
+Proof.
+ unfold adapt. intros Hf x y EQ.
+ destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT'].
+ - now apply eq_add_S, Hf.
+ - apply Lt.le_lt_or_eq in LE.
+   destruct LE as [LT|EQ']; [|now apply Hf in EQ'].
+   unfold lt in LT. rewrite EQ in LT.
+   rewrite <- (Lt.S_pred _ _ LT') in LT.
+   elim (Lt.lt_not_le _ _ LT' LT).
+ - apply Lt.le_lt_or_eq in LE'.
+   destruct LE' as [LT'|EQ']; [|now apply Hf in EQ'].
+   unfold lt in LT'. rewrite <- EQ in LT'.
+   rewrite <- (Lt.S_pred _ _ LT) in LT'.
+   elim (Lt.lt_not_le _ _ LT LT').
+ - apply eq_add_S, Hf.
+   now rewrite (Lt.S_pred _ _ LT), (Lt.S_pred _ _ LT'), EQ.
+Qed.
+
+Let adapt_ok a l1 l2 f : injective f -> length l1 = f 0 ->
+ forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n).
+Proof.
+ unfold adapt. intros Hf E n.
+ destruct le_lt_dec as [LE|LT].
+ - apply Lt.le_lt_or_eq in LE.
+   destruct LE as [LT|EQ]; [|now apply Hf in EQ].
+   rewrite <- E in LT.
+   rewrite 2 nth_error_app1; auto.
+ - rewrite (Lt.S_pred _ _ LT) at 1.
+   rewrite <- E, (Lt.S_pred _ _ LT) in LT.
+   rewrite 2 nth_error_app2; auto with arith.
+   rewrite <- Minus.minus_Sn_m; auto with arith.
+Qed.
+
+Lemma Permutation_nth_error l l' :
+ Permutation l l' <->
+  (length l = length l' /\
+   exists f:nat->nat,
+    injective f /\ forall n, nth_error l' n = nth_error l (f n)).
+Proof.
+ split.
+ { intros P.
+   split; [now apply Permutation_length|].
+   induction P.
+   - exists (fun n => n).
+     split; try red; auto.
+   - destruct IHP as (f & Hf & Hf').
+     exists (fun n => match n with O => O | S n => S (f n) end).
+     split; try red.
+     * intros [|y] [|z]; simpl; now auto.
+     * intros [|n]; simpl; auto.
+   - exists (fun n => match n with 0 => 1 | 1 => 0 | n => n end).
+     split; try red.
+     * intros [|[|z]] [|[|t]]; simpl; now auto.
+     * intros [|[|n]]; simpl; auto.
+   - destruct IHP1 as (f & Hf & Hf').
+     destruct IHP2 as (g & Hg & Hg').
+     exists (fun n => f (g n)).
+     split; try red.
+     * auto.
+     * intros n. rewrite <- Hf'; auto. }
+ { revert l. induction l'.
+   - intros [|l] (E & _); now auto.
+   - intros l (E & f & Hf & Hf').
+     simpl in E.
+     assert (Ha : nth_error l (f 0) = Some a)
+      by (symmetry; apply (Hf' 0)).
+     destruct (nth_error_split l (f 0) Ha) as (l1 & l2 & L12 & L1).
+     rewrite L12. rewrite <- Permutation_middle. constructor.
+     apply IHl'; split; [|exists (adapt f); split].
+     * revert E. rewrite L12, !app_length. simpl.
+       rewrite <- plus_n_Sm. now injection 1.
+     * now apply adapt_injective.
+     * intro n. rewrite <- (adapt_ok a), <- L12; auto.
+       apply (Hf' (S n)). }
+Qed.
+
+Lemma Permutation_nth_error_bis l l' :
+ Permutation l l' <->
+  exists f:nat->nat,
+    injective f /\
+    (forall n, n < length l -> f n < length l) /\
+    (forall n, nth_error l' n = nth_error l (f n)).
+Proof.
+ rewrite Permutation_nth_error; split.
+ - intros (E & f & Hf & Hf').
+   exists f. do 2 (split; trivial).
+   intros n Hn.
+   destruct (Lt.le_or_lt (length l) (f n)) as [LE|LT]; trivial.
+   rewrite <- nth_error_None, <- Hf', nth_error_None, <- E in LE.
+   elim (Lt.lt_not_le _ _ Hn LE).
+ - intros (f & Hf & Hf2 & Hf3); split; [|exists f; auto].
+   assert (H : length l' <= length l') by auto with arith.
+   rewrite <- nth_error_None, Hf3, nth_error_None in H.
+   destruct (Lt.le_or_lt (length l) (length l')) as [LE|LT];
+    [|apply Hf2 in LT; elim (Lt.lt_not_le _ _ LT H)].
+   apply Lt.le_lt_or_eq in LE. destruct LE as [LT|EQ]; trivial.
+   rewrite <- nth_error_Some, Hf3, nth_error_Some in LT.
+   destruct (injective_bounded_surjective Hf Hf2 LT) as (y & Hy & Hy').
+   apply Hf in Hy'. subst y. elim (Lt.lt_irrefl _ Hy).
+Qed.
+
+Lemma Permutation_nth l l' d :
+ Permutation l l' <->
+  (let n := length l in
+   length l' = n /\
+   exists f:nat->nat,
+    (forall x, x < n -> f x < n) /\
+    (forall x y, x < n -> y < n -> f x = f y -> x = y) /\
+    (forall x, x < n -> nth x l' d = nth (f x) l d)).
+Proof.
+ split.
+ - intros H.
+   assert (E := Permutation_length H).
+   split; auto.
+   apply Permutation_nth_error_bis in H.
+   destruct H as (f & Hf & Hf2 & Hf3).
+   exists f. split; [|split]; auto.
+   intros n Hn. rewrite <- 2 nth_default_eq. unfold nth_default.
+    now rewrite Hf3.
+ - intros (E & f & Hf1 & Hf2 & Hf3).
+   rewrite Permutation_nth_error.
+   split; auto.
+   exists (fun n => if le_lt_dec (length l) n then n else f n).
+   split.
+   * intros x y.
+     destruct le_lt_dec as [LE|LT];
+      destruct le_lt_dec as [LE'|LT']; auto.
+     + apply Hf1 in LT'. intros ->.
+       elim (Lt.lt_irrefl (f y)). eapply Lt.lt_le_trans; eauto.
+     + apply Hf1 in LT. intros <-.
+       elim (Lt.lt_irrefl (f x)). eapply Lt.lt_le_trans; eauto.
+   * intros n.
+     destruct le_lt_dec as [LE|LT].
+     + assert (LE' : length l' <= n) by (now rewrite E).
+       rewrite <- nth_error_None in LE, LE'. congruence.
+     + assert (LT' : n < length l') by (now rewrite E).
+       specialize (Hf3 n LT). rewrite <- 2 nth_default_eq in Hf3.
+       unfold nth_default in Hf3.
+       apply Hf1 in LT.
+       rewrite <- nth_error_Some in LT, LT'.
+       do 2 destruct nth_error; congruence.
+Qed.
+
+End Permutation_alt.
+
+(* begin hide *)
+Notation Permutation_app_swap := Permutation_app_comm (only parsing).
+(* end hide *)

samples/Coq/Poly.v

@@ -0,0 +1,875 @@
+Require Export Lists.
+Require Export Basics.
+
+Import Playground1.
+
+Inductive list (X : Type) : Type :=
+	| nil : list X
+	| cons : X -> list X -> list X.
+
+Fixpoint length (X:Type) (l:list X) : nat :=
+	match l with
+		| nil => O
+		| cons h t => S (length X t)
+	end.
+
+Fixpoint app (X : Type) (l1 l2 : list X)
+										: (list X) :=
+	match l1 with
+		| nil => l2
+		| cons h t => cons X h (app X t l2)
+	end.
+
+Fixpoint snoc (X:Type) (l:list X) (v:X) : (list X) :=
+	match l with
+		| nil => cons X v (nil X)
+		| cons h t => cons X h (snoc X t v)
+	end.
+
+Fixpoint rev (X:Type) (l:list X) : list X :=
+	match l with
+		| nil => nil X
+		| cons h t => snoc X (rev X t) h
+	end.
+
+
+Implicit Arguments nil [[X]].
+Implicit Arguments cons [[X]].
+Implicit Arguments length [[X]].
+Implicit Arguments app [[X]].
+Implicit Arguments rev [[X]].
+Implicit Arguments snoc [[X]].
+
+Definition list123 := cons 1 (cons 2 (cons 3 (nil))).
+
+Notation "x :: y" := (cons x y) (at level 60, right associativity).
+Notation "[]" := nil.
+Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
+Notation "x ++ y" := (app x y) (at level 60, right associativity).
+
+Fixpoint repeat (X : Type) (n : X) (count : nat) : list X :=
+	match count with
+		| O => nil
+		| S count' => n :: (repeat _ n count')
+	end.
+
+Example test_repeat1:
+	repeat bool true (S (S O)) = [true, true].
+Proof. reflexivity. Qed.
+
+Theorem nil_app : forall X:Type, forall l:list X,
+	app [] l = l.
+Proof.
+	reflexivity.
+	Qed.
+
+Theorem rev_snoc : forall X : Type,
+									 forall v : X,
+									 forall s : list X,
+	rev (snoc s v) = v :: (rev s).
+Proof.
+	intros X v s.
+	induction s.
+		reflexivity.
+		simpl.
+		rewrite -> IHs.
+		reflexivity.
+		Qed.
+
+Theorem snoc_with_append : forall X : Type,
+													 forall l1 l2 : list X,
+													 forall v : X,
+	snoc (l1 ++ l2) v = l1 ++ (snoc l2 v).
+Proof.
+	intros X l1 l2 v.
+	induction l1.
+		reflexivity.
+		simpl.
+		rewrite -> IHl1.
+		reflexivity.
+		Qed.
+
+Inductive prod (X Y : Type) : Type :=
+	pair : X -> Y -> prod X Y.
+
+Implicit Arguments pair [X Y].
+
+Notation "( x , y )" := (pair x y).
+Notation "X * Y" := (prod X Y) : type_scope.
+
+Definition fst (X Y : Type) (p : X * Y) : X :=
+	match p with (x,y) => x end.
+Definition snd (X Y : Type) (p : X * Y) : Y :=
+	match p with (x,y) => y end.
+
+Fixpoint combine (X Y : Type) (lx : list X) (ly : list Y)
+			: list (X * Y) :=
+	match lx, ly with
+		| [], _ => []
+		| _,[] => []
+		| x::tx, y::ty => (x,y) :: (combine _ _ tx ty)
+	end.
+
+Implicit Arguments combine [X Y].
+
+Fixpoint split {X Y: Type} (s : list (X * Y)) : (list X)*(list Y) :=
+	match s with
+		| nil => (nil, nil)
+		| (x,y) :: tp => match split tp with
+											| (lx, ly) => (x :: lx, y :: ly)
+										 end
+	end.
+
+Inductive option (X : Type) : Type :=
+	| Some : X -> option X
+	| None : option X.
+
+Implicit Arguments Some [X].
+Implicit Arguments None [X].
+
+Fixpoint index (X : Type) (n : nat)
+							 (l : list X) : option X :=
+	match n with
+		| O => match l with
+								| nil => None
+								| x :: xs => Some x
+					 end
+		| S n' => match l with
+									| nil => None
+									| x :: xs => index X n' xs
+							end
+	end.
+
+Definition hd_opt (X : Type) (l : list X) : option X :=
+		match l with
+			| nil => None
+			| x :: xs => Some x
+		end.
+
+Implicit Arguments hd_opt [X].
+
+Example test_hd_opt1 : hd_opt [S O, S (S O)] = Some (S O).
+Proof. reflexivity. Qed.
+Example test_hd_opt2 : hd_opt [[S O], [S (S O)]] = Some [S O].
+Proof. reflexivity. Qed.
+
+Definition plus3 := plus (S (S (S O))).
+
+Definition prod_curry {X Y Z : Type}
+		(f : X * Y -> Z) (x : X) (y : Y) : Z := f (x,y).
+
+Definition prod_uncurry {X Y Z : Type}
+	(f : X -> Y -> Z) (p : X * Y) : Z :=
+	f (fst X Y p) (snd X Y p).
+
+Theorem uncurry_uncurry : forall (X Y Z : Type) (f : X -> Y -> Z) x y,
+				prod_curry (prod_uncurry f) x y = f x y.
+Proof.
+	reflexivity.
+Qed.
+
+Theorem curry_uncurry : forall (X Y Z : Type) (f : (X * Y) -> Z)
+	(p : X * Y),
+		prod_uncurry (prod_curry f) p = f p.
+Proof.
+	destruct p.
+	reflexivity.
+	Qed.
+
+Fixpoint filter (X : Type) (test : X -> bool) (l:list X)
+				: (list X) :=
+		match l with
+			| [] => []
+		  | h :: t => if test h then h :: (filter _ test t)
+									else filter _ test t
+		end.
+
+Definition countoddmembers' (l:list nat) : nat :=
+	length (filter _ oddb l).
+
+Definition partition (X : Type) (test : X -> bool) (l : list X)
+							: list X * list X :=
+	(filter _ test l, filter _ (fun el => negb (test el)) l).
+
+Example test_partition1: partition _ oddb [S O, S (S O), S (S (S O)), S (S (S (S O))), S (S (S (S (S O))))] = ([S O, S (S (S O)), S (S (S (S (S O))))], [S (S O), S (S (S (S O)))]).
+Proof. reflexivity. Qed.
+
+Fixpoint map {X Y : Type} (f : X -> Y) (l : list X) : (list Y ) :=
+		match l with
+			| [] => []
+			| h :: t => (f h) :: (map f t)
+		end.
+
+Example test_map1: map (plus (S (S (S O)))) [S (S O), O, S (S O)] = [S (S (S (S (S O)))), S (S (S O)), S (S (S (S (S O))))].
+Proof. reflexivity. Qed.
+
+ Theorem map_rev_1 : forall (X Y: Type) (f: X -> Y) (l : list X) (x : X),
+ 		map f (snoc l x) = snoc (map f l) (f x).
+Proof.
+	intros X Y f l x.
+	induction l.
+	reflexivity.
+	simpl.
+	rewrite -> IHl.
+	reflexivity.
+	Qed.
+
+Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
+				map f (rev l) = rev (map f l).
+Proof.
+	intros X Y f l.
+	induction l.
+		reflexivity.
+		simpl.
+		rewrite <- IHl.
+		rewrite -> map_rev_1.
+		reflexivity.
+		Qed.
+
+Fixpoint flat_map {X Y : Type} (f : X -> list Y) (l : list X)
+			: (list Y) :=
+	match l with
+		| [] => []
+		| x :: xs => (f x) ++ (flat_map f xs)
+	end.
+
+Definition map_option {X Y : Type} (f : X -> Y) (xo : option X)
+		: option Y :=
+	match xo with
+		| None => None
+		| Some x => Some (f x)
+	end.
+
+Fixpoint fold {X Y: Type} (f: X -> Y -> Y) (l:list X) (b:Y) : Y :=
+	match l with
+		| nil => b
+		| h :: t => f h (fold f t b)
+	end.
+
+Example fold_example : fold andb [true, true, false, true] true = false.
+Proof. reflexivity. Qed.
+
+Definition constfun {X : Type} (x: X) : nat -> X :=
+	fun (k:nat) => x.
+
+Definition ftrue := constfun true.
+Example constfun_example : ftrue O = true.
+Proof. reflexivity. Qed.
+
+Definition override {X : Type} (f: nat -> X) (k:nat) (x:X) : nat->X :=
+	fun (k':nat) => if beq_nat k k' then x else f k'.
+
+Definition fmostlytrue := override (override ftrue (S O) false) (S (S (S O))) false.
+
+Example override_example1 : fmostlytrue O = true.
+Proof. reflexivity. Qed.
+Example override_example2 : fmostlytrue (S O) = false.
+Proof. reflexivity. Qed.
+Example override_example3 : fmostlytrue (S (S O)) = true.
+Proof. reflexivity. Qed.
+Example override_example4 : fmostlytrue (S (S (S O))) = false.
+Proof. reflexivity. Qed.
+
+Theorem override_example : forall (b: bool),
+	(override (constfun b) (S (S (S O))) true) (S (S O)) = b.
+Proof.
+	reflexivity.
+Qed.
+
+Theorem unfold_example_bad : forall m n,
+	(S (S (S O))) + n = m ->
+	plus3 n = m.
+Proof.
+	intros m n H.
+	unfold plus3.
+	rewrite -> H.
+	reflexivity.
+	Qed.
+
+Theorem override_eq : forall {X : Type} x k (f : nat -> X),
+	(override f k x) k = x.
+Proof.
+	intros X x k f.
+	unfold override.
+	rewrite <- beq_nat_refl.
+	reflexivity.
+	Qed.
+
+Theorem override_neq : forall {X : Type} x1 x2 k1 k2 (f : nat->X),
+	f k1 = x1 ->
+		beq_nat k2 k1 = false ->
+			(override f k2 x2) k1 = x1.
+Proof.
+	intros X x1 x2 k1 k2 f eq1 eq2.
+	unfold override.
+	rewrite -> eq2.
+	rewrite -> eq1.
+	reflexivity.
+Qed.
+
+Theorem eq_add_S : forall (n m : nat),
+	S n = S m ->
+		n = m.
+Proof.
+	intros n m eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem silly4 : forall (n m : nat),
+	[n] = [m] ->
+		n = m.
+Proof.
+	intros n o eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem silly5 : forall (n m o : nat),
+	[n,m] = [o,o] ->
+		[n] = [m].
+Proof.
+	intros n m o eq.
+	inversion eq.
+	reflexivity.
+Qed.
+
+Theorem sillyex1 : forall (X : Type) (x y z : X) (l j : list X),
+	x :: y :: l = z :: j ->
+		y :: l = x :: j ->
+			x = y.
+Proof.
+	intros X x y z l j.
+	intros eq1 eq2.
+	inversion eq1.
+	inversion eq2.
+	symmetry.
+	rewrite -> H0.
+	reflexivity.
+Qed.
+
+Theorem silly6 : forall (n : nat),
+	S n = O ->
+		(S (S O)) + (S (S O)) = (S (S (S (S (S O))))).
+Proof.
+	intros n contra.
+	inversion contra.
+Qed.
+
+Theorem silly7 : forall (n m : nat),
+				false = true ->
+					[n] = [m].
+Proof.
+	intros n m contra.
+	inversion contra.
+Qed.
+
+Theorem sillyex2 : forall (X : Type) (x y z : X) (l j : list X),
+	x :: y :: l = [] ->
+		y :: l = z :: j ->
+			x = z.
+Proof.
+	intros X x y z l j contra.
+	inversion contra.
+	Qed.
+
+Theorem beq_nat_eq : forall n m,
+	true = beq_nat n m -> n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		intros m. destruct m as [| m'].
+		SCase "m = 0". reflexivity.
+		SCase "m = S m'". simpl. intros contra. inversion contra.
+	Case "n = S n'".
+		intros m. destruct m as [| m'].
+		SCase "m = 0". simpl. intros contra. inversion contra.
+		SCase "m = S m'". simpl. intros H.
+			assert(n' = m') as Hl.
+				SSCase "Proof of assertion". apply IHn'. apply H.
+			rewrite -> Hl. reflexivity.
+Qed.
+
+Theorem beq_nat_eq' : forall m n,
+				beq_nat n m = true -> n = m.
+Proof.
+	intros m. induction m as [| m'].
+	Case "m = O".
+		destruct n.
+		SCase "n = O".
+			reflexivity.
+		SCase "n = S n'".
+			simpl. intros contra. inversion contra.
+	Case "m = S m'".
+		simpl.
+		destruct n.
+		SCase "n = O".
+			simpl. intros contra. inversion contra.
+		SCase "n = S n'".
+			simpl. intros H.
+			assert (n = m') as Hl.
+				apply IHm'.
+				apply H.
+			rewrite -> Hl.
+			reflexivity.
+Qed.
+
+Theorem length_snoc' : forall (X : Type) (v : X)
+(l : list X) (n : nat),
+	length l = n ->
+	length (snoc l v) = S n.
+	Proof.
+	intros X v l. induction l as [| v' l'].
+	Case "l = []". intros n eq. rewrite <- eq. reflexivity.
+	Case "l = v' :: l'". intros n eq. simpl. destruct n as [| n'].
+	SCase "n = 0". inversion eq.
+	SCase "n = S n'".
+	assert (length (snoc l' v) = S n').
+	SSCase "Proof of assertion". apply IHl'.
+	inversion eq. reflexivity.
+	rewrite -> H. reflexivity.
+	Qed.
+
+	Theorem beq_nat_O_l : forall n,
+	true = beq_nat O n -> O = n.
+	Proof.
+	intros n. destruct n.
+	reflexivity.
+	simpl.
+	intros contra.
+	inversion contra.
+	Qed.
+
+Theorem beq_nat_O_r : forall n,
+	true = beq_nat n O -> O = n.
+Proof.
+	intros n.
+	induction n.
+	Case "n = O".
+		reflexivity.
+	Case "n = S n'".
+		simpl.
+		intros contra.
+		inversion contra.
+	Qed.
+
+Theorem double_injective : forall n m,
+	double n = double m ->
+		n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		simpl. intros m eq.
+		destruct m as [|m'].
+		SCase "m = O". reflexivity.
+		SCase "m = S m'". inversion eq.
+	Case "n = S n'". intros m eq. destruct m as [| m'].
+		SCase "m = O". inversion eq.
+		SCase "m = S m'".
+			assert(n' = m') as H.
+				SSCase "Proof of assertion". apply IHn'. inversion eq. reflexivity.
+			rewrite -> H. reflexivity.
+Qed.
+
+Theorem silly3' : forall (n : nat),
+	(beq_nat n (S (S (S (S (S O))))) = true ->
+	 	beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))) = true) ->
+		true = beq_nat n (S (S (S (S (S O))))) ->
+			true = beq_nat (S (S n)) (S (S (S (S (S (S (S O))))))).
+Proof.
+	intros n eq H.
+	symmetry in H.
+	apply eq in H.
+	symmetry in H.
+	apply H.
+Qed.
+
+Theorem plus_n_n_injective : forall n m,
+					n + n = m + m ->
+						n = m.
+Proof.
+	intros n. induction n as [| n'].
+	Case "n = O".
+		simpl. intros m.
+		destruct m.
+			SCase "m = O".
+			reflexivity.
+			SCase "m = S m'".
+			simpl.
+			intros contra.
+			inversion contra.
+	Case "n = S n".
+		intros m.
+		destruct m.
+			SCase "m = O".
+			intros contra.
+			inversion contra.
+			SCase "m = S m'".
+			intros eq.
+			inversion eq.
+			rewrite <- plus_n_Sm in H0.
+			rewrite <- plus_n_Sm in H0.
+			inversion H0.
+			apply IHn' in H1.
+			rewrite -> H1.
+			reflexivity.
+	Qed.
+
+Theorem override_shadow : forall {X : Type} x1 x2 k1 k2 (f : nat -> X),
+	(override (override f k1 x2) k1 x1) k2 = (override f k1 x1) k2.
+Proof.
+	intros X x1 x2 k1 k2 f.
+	unfold override.
+	destruct (beq_nat k1 k2).
+	reflexivity.
+	reflexivity.
+	Qed.
+
+Theorem combine_split : forall (X : Type) (Y : Type) (l : list (X * Y)) (l1: list X) (l2: list Y),
+				split l = (l1, l2) -> combine l1 l2 = l.
+Proof.
+	intros X Y l.
+	induction l as [| x y].
+	Case "l = nil".
+		intros l1 l2.
+		intros eq.
+		simpl.
+		simpl in eq.
+		inversion eq.
+		reflexivity.
+	Case "l = ::".
+		intros l1 l2.
+		simpl.
+		destruct x.
+		destruct (split y).
+		simpl.
+		destruct l1.
+		SCase "l1 = []".
+			simpl.
+			induction l2.
+			SSCase "l2 = []".
+				intros contra.
+				inversion contra.
+			SSCase "l2 = ::".
+				intros contra.
+				inversion contra.
+		SCase "l1 = ::".
+			induction l2.
+			SSCase "l2 = []".
+				simpl.
+				intros contra.
+				inversion contra.
+			SSCase "l2 = ::".
+				simpl.
+				intros eq.
+				inversion eq.
+				simpl.
+				rewrite IHy.
+				reflexivity.
+				simpl.
+				rewrite H1.
+				rewrite H3.
+				reflexivity.
+Qed.
+
+Theorem split_combine : forall (X : Type) (Y : Type) (l1: list X) (l2: list Y),
+				length l1 = length l2 -> split (combine l1 l2) = (l1, l2).
+Proof.
+intros X Y.
+intros l1.
+induction l1.
+simpl.
+intros l2.
+induction l2.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct l2.
+simpl.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+inversion eq.
+apply IHl1 in H0.
+rewrite H0.
+reflexivity.
+Qed.
+
+Definition sillyfun1 (n : nat) : bool :=
+	 if beq_nat n (S (S (S O))) then true
+	 else if beq_nat n (S (S (S (S (S O))))) then true
+				else false.
+
+Theorem beq_equal : forall (a b : nat),
+		beq_nat a b = true ->
+			a = b.
+Proof.
+intros a.
+induction a.
+destruct b.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct b.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+apply IHa in eq.
+rewrite eq.
+reflexivity.
+Qed.
+
+Theorem override_same : forall {X : Type} x1 k1 k2 (f : nat->X),
+	f k1 = x1 ->
+		(override f k1 x1) k2 = f k2.
+Proof.
+	intros X x1 k1 k2 f eq.
+	unfold override.
+	remember (beq_nat k1 k2) as a.
+	destruct a.
+	rewrite <- eq.
+	symmetry in Heqa.
+	apply beq_equal in Heqa.
+	rewrite -> Heqa.
+	reflexivity.
+	reflexivity.
+	Qed.
+
+
+Theorem filter_exercise : forall (X : Type) (test : X -> bool)
+	(x : X) (l lf : list X),
+	filter _ test l = x :: lf ->
+		test x = true.
+Proof.
+intros X.
+intros test.
+intros x.
+induction l.
+simpl.
+intros lf.
+intros contra.
+inversion contra.
+
+simpl.
+remember (test x0) as a.
+destruct a.
+simpl.
+intros lf.
+intros eq.
+rewrite Heqa.
+inversion eq.
+reflexivity.
+
+intros lf.
+intros eq.
+apply IHl in eq.
+rewrite eq.
+reflexivity.
+Qed.
+
+Theorem trans_eq : forall {X:Type} (n m o : X),
+				n = m -> m = o -> n = o.
+Proof.
+	intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2.
+	reflexivity.
+Qed.
+
+Example trans_eq_example' : forall (a b c d e f : nat),
+				[a,b] = [c,d] ->
+				[c,d] = [e,f] ->
+				[a,b] = [e,f].
+Proof.
+	intros a b c d e f eq1 eq2.
+	apply trans_eq with (m := [c,d]). apply eq1. apply eq2.
+	Qed.
+
+Theorem trans_eq_exercise : forall (n m o p : nat),
+		m = (minustwo o) ->
+		(n + p) = m ->
+		(n + p) = (minustwo o).
+Proof.
+intros n m o p.
+intros eq1 eq2.
+rewrite eq2.
+rewrite <- eq1.
+reflexivity.
+Qed.
+
+Theorem beq_nat_trans : forall n m p,
+				true = beq_nat n m ->
+				true = beq_nat m p ->
+				true = beq_nat n p.
+Proof.
+intros n m p.
+intros eq1 eq2.
+symmetry  in eq1.
+symmetry  in eq2.
+apply beq_equal in eq1.
+apply beq_equal in eq2.
+rewrite eq1.
+rewrite <- eq2.
+apply beq_nat_refl.
+Qed.
+
+Theorem override_permute : forall {X:Type} x1 x2 k1 k2 k3 (f : nat->X),
+	false = beq_nat k2 k1 ->
+	(override (override f k2 x2) k1 x1) k3 = (override (override f k1 x1) k2 x2) k3.
+Proof.
+intros X x1 x2 k1 k2 k3 f.
+simpl.
+unfold override.
+remember (beq_nat k1 k3).
+remember (beq_nat k2 k3).
+destruct b.
+destruct b0.
+symmetry  in Heqb.
+symmetry  in Heqb0.
+apply beq_equal in Heqb.
+apply beq_equal in Heqb0.
+rewrite <- Heqb in Heqb0.
+assert (k2 = k1 -> true = beq_nat k2 k1).
+destruct k2.
+destruct k1.
+reflexivity.
+
+intros contra.
+inversion contra.
+
+destruct k1.
+intros contra.
+inversion contra.
+
+simpl.
+intros eq.
+inversion eq.
+symmetry .
+symmetry .
+apply beq_nat_refl.
+
+apply H in Heqb0.
+rewrite <- Heqb0.
+intros contra.
+inversion contra.
+
+intros eq.
+reflexivity.
+
+destruct b0.
+intros eq.
+reflexivity.
+
+intros eq.
+reflexivity.
+
+Qed.
+
+Definition fold_length {X : Type} (l : list X) : nat :=
+	fold (fun _ n => S n) l O.
+
+Example test_fold_length1 : fold_length [S (S (S (S O))), S (S (S (S (S (S (S O)))))), O] = S (S (S O)).
+Proof. reflexivity. Qed.
+
+Theorem fold_length_correct : forall X (l :list X),
+	fold_length l = length l.
+Proof.
+	intros X l.
+	unfold fold_length.
+	induction l.
+	Case "l = O".
+		reflexivity.
+	Case "l = ::".
+		simpl.
+		rewrite IHl.
+		reflexivity.
+	Qed.
+
+Definition fold_map {X Y: Type} (f : X -> Y) (l : list X) : list Y :=
+	fold (fun x total => (f x) :: total) l [].
+
+Theorem fold_map_correct : forall (X Y: Type) (f : X -> Y) (l : list X),
+	fold_map f l = map f l.
+Proof.
+	intros X Y f l.
+	unfold fold_map.
+	induction l.
+	reflexivity.
+	  
+	simpl.
+	rewrite IHl.
+	reflexivity.
+	Qed.
+
+Fixpoint forallb {X : Type} (f : X -> bool) (l : list X) :=
+	match l with
+		| nil => true
+		| x :: xs => andb (f x) (forallb f xs)
+	end.
+
+Fixpoint existsb {X : Type} (f : X -> bool) (l : list X) :=
+	match l with
+		| nil => false
+		| x :: xs => orb (f x) (existsb f xs)
+	end.
+
+Definition existsb2 {X : Type} (f: X -> bool) (l : list X) :=
+	negb (forallb (fun x => negb (f x)) l).
+
+Theorem existsb_correct : forall (X : Type) (f : X -> bool) (l : list X),
+		existsb f l = existsb2 f l.
+Proof.
+intros X f l.
+induction l.
+reflexivity.
+
+simpl.
+rewrite IHl.
+unfold existsb2.
+simpl.
+destruct (forallb (fun x0 : X => negb (f x0)) l).
+simpl.
+destruct (f x).
+reflexivity.
+
+reflexivity.
+
+destruct (f x).
+reflexivity.
+
+reflexivity.
+
+Qed.
+
+Theorem index_okx : forall (X:Type) (l : list X) (n : nat),
+		length l = n -> index X (S n) l = None.
+Proof.
+	intros X l.
+	induction l.
+	reflexivity.
+
+	intros n.
+	destruct n.
+	intros contra.
+	inversion contra.
+
+	intros eq.
+	inversion eq.
+	apply IHl.
+	reflexivity.
+Qed.
+
+Inductive mumble : Type :=
+  | a : mumble
+	| b : mumble -> nat -> mumble
+	| c : mumble.
+Inductive grumble (X:Type) : Type :=
+ | d : mumble -> grumble X
+ | e : X -> grumble X.
+

samples/Coq/Rel.v

@@ -0,0 +1,312 @@
+Require Export Logic.
+Import Playground1.
+
+Definition relation (X:Type) := X -> X -> Prop.
+
+Definition partial_function {X:Type} (R: relation X) :=
+	forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
+
+Theorem next_nat_partial_function :
+	partial_function next_nat.
+Proof.
+	unfold partial_function.
+	intros x y1 y2 P Q.
+	inversion P.
+	inversion Q.
+	reflexivity.
+Qed.
+
+Theorem le_not_a_partial_function :
+	~ (partial_function le).
+Proof.
+	unfold not.
+	unfold partial_function.
+	intros H.
+	assert (O = S O) as Nonsense.
+		Case "Proof of assertion.".
+		apply H with O.
+		apply le_n.
+
+		apply le_S.
+		apply le_n.
+
+	inversion Nonsense.
+Qed.
+
+Theorem total_relation_not_partial_function :
+	~ (partial_function total_relation).
+Proof.
+	unfold not.
+	unfold partial_function.
+	intros H.
+	assert (O = S O) as Nonsense.
+	apply H with O.
+	apply total_relation1.
+
+	apply total_relation1.
+
+	inversion Nonsense.
+Qed.
+
+Theorem empty_relation_not_partial_funcion :
+	partial_function empty_relation.
+Proof.
+	unfold partial_function.
+	intros x y1 y2.
+	intros H.
+	inversion H.
+Qed.
+
+Definition reflexive {X:Type} (R: relation X) :=
+	forall a : X, R a a.
+
+Theorem le_reflexive :
+	reflexive le.
+Proof.
+	unfold reflexive.
+	intros n. apply le_n.
+Qed.
+
+Definition transitive {X:Type} (R: relation X) :=
+	forall a b c : X, (R a b) -> (R b c) -> (R a c).
+
+Theorem le_trans:
+	transitive le.
+Proof.
+	intros n m o Hnm Hmo.
+	induction Hmo.
+	Case "le_n". apply Hnm.
+	Case "le_S". apply le_S. apply IHHmo.
+Qed.
+
+Theorem lt_trans:
+	transitive lt.
+Proof.
+	unfold lt. unfold transitive.
+	intros n m o Hnm Hmo.
+	apply le_S in Hnm.
+	apply le_trans with (a := (S n)) (b := (S m)) (c := o).
+	apply Hnm.
+	apply Hmo.
+Qed.
+
+Theorem lt_trans' :
+	transitive lt.
+Proof.
+	unfold lt. unfold transitive.
+	intros n m o Hnm Hmo.
+	induction Hmo as [| m' Hm'o].
+	apply le_S.
+	apply Hnm.
+
+	apply le_S.
+	apply IHHm'o.
+Qed.
+
+Theorem le_Sn_le: forall n m, S n <= m -> n <= m.
+Proof.
+	intros n m H. apply le_trans with (S n).
+	apply le_S. apply le_n.
+	apply H. Qed.
+
+Theorem le_S_n : forall n m,
+	(S n <= S m) -> (n <= m).
+Proof.
+intros n m H.
+apply Sn_le_Sm__n_le_m.
+apply H.
+Qed.
+
+Theorem le_Sn_n : forall n,
+	~ (S n <= n).
+Proof.
+induction n.
+intros H.
+inversion H.
+
+unfold not in IHn.
+intros H.
+apply le_S_n in H.
+apply IHn.
+apply H.
+Qed.
+
+(*
+ TODO
+Theorem lt_trans'' :
+	transitive lt.
+Proof.
+	unfold lt. unfold transitive.
+	intros n m o Hnm Hmo.
+	induction o as [| o'].
+	*)
+
+Definition symmetric {X: Type} (R: relation X) :=
+	forall a b : X, (R a b) -> (R b a).
+
+Definition antisymmetric {X : Type} (R: relation X) :=
+	forall a b : X, (R a b) -> (R b a) -> a = b.
+
+Theorem le_antisymmetric :
+	antisymmetric le.
+Proof.
+intros a b.
+generalize dependent a.
+induction b.
+intros a.
+intros H.
+intros H1.
+inversion H.
+reflexivity.
+
+intros a H1 H2.
+destruct a.
+inversion H2.
+
+apply Sn_le_Sm__n_le_m in H1.
+apply Sn_le_Sm__n_le_m in H2.
+apply IHb in H1.
+rewrite H1 in |- *.
+reflexivity.
+
+apply H2.
+Qed.
+
+(*
+ TODO
+Theorem le_step : forall n m p,
+	n < m ->
+	n <= S p ->
+	n <= p.
+Proof.
+*)
+
+Definition equivalence {X:Type} (R: relation X) :=
+	(reflexive R) /\ (symmetric R) /\ (transitive R).
+
+Definition order {X:Type} (R: relation X) :=
+	(reflexive R) /\ (antisymmetric R) /\ (transitive R).
+
+Definition preorder {X:Type} (R: relation X) :=
+	(reflexive R) /\ (transitive R).
+
+Theorem le_order :
+	order le.
+Proof.
+	unfold order. split.
+	Case "refl". apply le_reflexive.
+	split.
+		Case "antisym". apply le_antisymmetric.
+		Case "transitive". apply le_trans. Qed.
+
+Inductive clos_refl_trans {A:Type} (R: relation A) : relation A :=
+	| rt_step : forall x y, R x y -> clos_refl_trans R x y
+	| rt_refl : forall x, clos_refl_trans R x x
+	| rt_trans : forall x y z,
+		clos_refl_trans R x y -> clos_refl_trans R y z -> clos_refl_trans R x z.
+
+Theorem next_nat_closure_is_le : forall n m,
+	(n <= m) <-> ((clos_refl_trans next_nat) n m).
+Proof.
+intros n m.
+split.
+intro H.
+induction H.
+apply rt_refl.
+
+apply rt_trans with m.
+apply IHle.
+
+apply rt_step.
+apply nn.
+
+intro H.
+induction H.
+inversion H.
+apply le_S.
+apply le_n.
+
+apply le_n.
+
+apply le_trans with y.
+apply IHclos_refl_trans1.
+
+apply IHclos_refl_trans2.
+Qed.																    
+
+Inductive refl_step_closure {X : Type} (R: relation X)
+											: X -> X -> Prop :=
+	| rsc_refl : forall (x : X), refl_step_closure R x x
+	| rsc_step : forall (x y z : X), R x y ->
+								refl_step_closure R y z ->
+								refl_step_closure R x z.
+
+Tactic Notation "rt_cases" tactic(first) ident(c) :=
+	first;
+	[ Case_aux c "rt_step" | Case_aux c "rt_refl" | Case_aux c "rt_trans" ].
+
+Tactic Notation "rsc_cases" tactic(first) ident(c) :=
+	  first;
+		  [ Case_aux c "rsc_refl" | Case_aux c "rsc_step" ].
+
+Theorem rsc_R : forall (X:Type) (R:relation X) (x y:X),
+				R x y -> refl_step_closure R x y.
+Proof.
+intros X R x y r.
+apply rsc_step with y.
+ apply r.
+  
+  apply rsc_refl.
+Qed.
+
+Theorem rsc_trans :
+	forall (X : Type) (R : relation X) (x y z : X),
+		refl_step_closure R x y ->
+			refl_step_closure R y z ->
+				refl_step_closure R x z.
+Proof.
+intros X.
+intros R x y z.
+intros H.
+induction H.
+intros H1.
+apply H1.
+
+intros H1.
+apply IHrefl_step_closure in H1.
+apply rsc_step with y.
+apply H.
+
+apply H1.
+Qed.
+
+Theorem rtc_rsc_coincide:
+	forall (X:Type) (R: relation X) (x y : X),
+		clos_refl_trans R x y <-> refl_step_closure R x y.
+Proof.
+intros X R x y.
+split.
+intros H.
+induction H.
+apply rsc_step with y.
+apply H.
+
+apply rsc_refl.
+
+apply rsc_refl.
+
+apply rsc_trans with y.
+apply IHclos_refl_trans1.
+
+apply IHclos_refl_trans2.
+
+intros H1.
+induction H1.
+apply rt_refl.
+
+apply rt_trans with y.
+apply rt_step.
+apply H.
+
+apply IHrefl_step_closure.
+Qed.

samples/Coq/Smallstep.v

@@ -0,0 +1,701 @@
+Require Export Imp.
+Require Export Relations.
+
+Inductive tm : Type :=
+   | tm_const : nat -> tm
+   | tm_plus : tm -> tm -> tm.
+
+Tactic Notation "tm_cases" tactic(first) ident(c) :=
+   first;
+   [ Case_aux c "tm_const" | Case_aux c "tm_plus" ].
+
+Module SimpleArith0.
+
+Fixpoint eval (t : tm) : nat :=
+   match t with
+      | tm_const n => n
+      | tm_plus a1 a2 => eval a1 + eval a2
+   end.
+
+End SimpleArith0.
+
+Module SimpleArith1.
+
+Reserved Notation " t '===>' n " (at level 50, left associativity).
+
+Inductive eval : tm -> nat -> Prop :=
+   | E_Const : forall n,
+                  tm_const n ===> n
+   | E_Plus : forall t1 t2 n1 n2,
+                  t1 ===> n1 ->
+                  t2 ===> n2 ->
+                  tm_plus t1 t2 ===> plus n1 n2
+
+     where " t '===>' n " := (eval t n).
+
+End SimpleArith1.
+
+Reserved Notation " t '===>' t' " (at level 50, left associativity).
+
+Inductive eval : tm -> tm -> Prop :=
+   | E_Const : forall n1,
+      tm_const n1 ===> tm_const n1
+   | E_Plus : forall t1 n1 t2 n2,
+      t1 ===> tm_const n1 ->
+      t2 ===> tm_const n2 ->
+         tm_plus t1 t2 ===> tm_const (plus n1 n2)
+   where " t '===>' t' " := (eval t t').
+
+Tactic Notation "eval_cases" tactic(first) ident(c) :=
+   first;
+   [ Case_aux c "E_Const" | Case_aux c "E_Plus" ].
+
+Module SimpleArith2.
+
+Reserved Notation " t '=>' t' " (at level 40).
+
+Inductive step : tm -> tm -> Prop :=
+   | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2) => tm_const (plus n1 n2)
+   | ST_Plus1 : forall t1 t1' t2,
+      t1 => t1' ->
+         tm_plus t1 t2 => tm_plus t1' t2
+   | ST_Plus2 : forall n1 t2 t2',
+      t2 => t2' ->
+      tm_plus (tm_const n1) t2 => tm_plus (tm_const n1) t2'
+
+   where " t '=>' t' " := (step t t').
+
+Tactic Notation "step_cases" tactic(first) ident(c) :=
+   first;
+   [ Case_aux c "ST_PlusConstConst"
+   | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
+
+Example test_step_1 : 
+      tm_plus 
+        (tm_plus (tm_const 0) (tm_const 3))
+        (tm_plus (tm_const 2) (tm_const 4))
+      =>
+      tm_plus 
+        (tm_const (plus 0 3))
+        (tm_plus (tm_const 2) (tm_const 4)).
+Proof.
+  apply ST_Plus1. apply ST_PlusConstConst. Qed.
+
+Example test_step_2 : 
+      tm_plus 
+        (tm_const 0)
+        (tm_plus 
+          (tm_const 2) 
+          (tm_plus (tm_const 0) (tm_const 3)))
+      =>
+      tm_plus 
+        (tm_const 0)
+        (tm_plus 
+          (tm_const 2) 
+          (tm_const (plus 0 3))).
+Proof.
+apply ST_Plus2.
+simpl.
+apply ST_Plus2.
+apply ST_PlusConstConst.
+Qed.
+
+Theorem step_deterministic:
+  partial_function step.
+Proof.
+  unfold partial_function. intros x y1 y2 Hy1 Hy2.
+  generalize dependent y2.
+  step_cases (induction Hy1) Case; intros y2 Hy2.
+    Case "ST_PlusConstConst". step_cases (inversion Hy2) SCase.
+      SCase "ST_PlusConstConst". reflexivity.
+      SCase "ST_Plus1". inversion H2.
+      SCase "ST_Plus2". inversion H2.
+    Case "ST_Plus1". step_cases (inversion Hy2) SCase.
+      SCase "ST_PlusConstConst". rewrite <- H0 in Hy1. inversion Hy1.
+      SCase "ST_Plus1".
+        rewrite <- (IHHy1 t1'0).
+        reflexivity. assumption.
+      SCase "ST_Plus2". rewrite <- H in Hy1. inversion Hy1.
+    Case "ST_Plus2". step_cases (inversion Hy2) SCase.
+      SCase "ST_PlusConstConst". rewrite <- H1 in Hy1. inversion Hy1.
+      SCase "ST_Plus1". inversion H2.
+      SCase "ST_Plus2".
+        rewrite <- (IHHy1 t2'0).
+        reflexivity. assumption. Qed.
+
+End SimpleArith2.
+
+Inductive value : tm -> Prop :=
+   v_const: forall n, value (tm_const n).
+
+Reserved Notation " t '=>' t' " (at level 40).
+
+Inductive step : tm -> tm -> Prop :=
+   | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2)
+         => tm_const (plus n1 n2)
+   | ST_Plus1 : forall t1 t1' t2,
+      t1 => t1' ->
+         tm_plus t1 t2 => tm_plus t1' t2
+   | ST_Plus2 : forall v1 t2 t2',
+      value v1 ->
+         t2 => t2' ->
+            tm_plus v1 t2 => tm_plus v1 t2'
+
+   where " t '=>' t' " := (step t t').
+
+Tactic Notation "step_cases" tactic(first) ident(c) :=
+   first;
+   [ Case_aux c "ST_PlusConstConst"
+      | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
+
+Theorem step_deterministic :
+   partial_function step.
+Proof.
+unfold partial_function.
+intros x y1 y2 Hy1 Hy2.
+generalize dependent y2.
+step_cases (induction Hy1) Case; intros y2 Hy2.
+ step_cases (inversion Hy2) SCase.
+  reflexivity.
+  
+  inversion H2.
+  
+  inversion Hy2.
+   subst.
+   assumption.
+   
+   subst.
+   inversion H3.
+   
+   subst.
+   inversion H3.
+   
+ step_cases (inversion Hy2) SCase.
+  rewrite <- H0 in Hy1.
+  inversion Hy1.
+  
+  rewrite <- (IHHy1 t1'0).
+   reflexivity.
+   
+   assumption.
+   
+  rewrite <- H in Hy1.
+  rewrite <- H in H1.
+  subst.
+  inversion H1.
+  subst.
+  inversion Hy1.
+  
+ step_cases (inversion Hy2) SCase.
+  subst.
+  inversion Hy1.
+  
+  subst.
+  inversion H.
+  subst.
+  inversion H3.
+  
+  subst.
+  inversion H2.
+  subst.
+  rewrite <- (IHHy1 t2'0).
+   reflexivity.
+   
+   assumption.
+Qed.
+
+Theorem strong_progress : forall t,
+        value t \/ (exists t', t => t').
+Proof.
+   tm_cases (induction t) Case.
+      Case "tm_const". left. apply v_const.
+      Case "tm_plus". right. inversion IHt1.
+         SCase "l". inversion IHt2.
+            SSCase "l". inversion H. inversion H0.
+               exists (tm_const (plus n n0)).
+               apply ST_PlusConstConst.
+            SSCase "r". inversion H0 as [t' H1].
+               exists (tm_plus t1 t').
+               apply ST_Plus2. apply H. apply H1.
+         SCase "r". inversion H as [t' H0].
+            exists (tm_plus t' t2).
+            apply ST_Plus1. apply H0. Qed.
+
+Definition normal_form {X:Type} (R: relation X) (t: X) : Prop :=
+    ~ (exists t', R t t'). 
+
+Lemma value_is_nf: forall t,
+      value t -> normal_form step t.
+Proof.
+   unfold normal_form. intros t H. inversion H.
+   intros contra. inversion contra. inversion H1.
+   Qed.
+
+Lemma nf_is_value: forall t,
+      normal_form step t -> value t.
+Proof.
+   unfold normal_form. intros t H.
+   assert (G: value t \/ (exists t', t => t')).
+      SCase "Proof of assertion". apply strong_progress.
+   inversion G.
+      SCase "l". assumption.
+      SCase "r". apply ex_falso_quodlibet. apply H. assumption. Qed.
+
+Corollary nf_same_as_value : forall t,
+            normal_form step t <-> value t.
+Proof.
+   split. apply nf_is_value. apply value_is_nf.
+Qed.
+
+Module Temp1.
+
+Inductive value : tm -> Prop :=
+| v_const : forall n, value (tm_const n)
+| v_funny : forall t1 n2, (* <---- *)
+              value (tm_plus t1 (tm_const n2)).
+
+Reserved Notation " t '=>' t' " (at level 40).
+
+Inductive step : tm -> tm -> Prop :=
+  | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2) => tm_const (plus n1 n2)
+  | ST_Plus1 : forall t1 t1' t2,
+      t1 => t1' ->
+      tm_plus t1 t2 => tm_plus t1' t2
+  | ST_Plus2 : forall v1 t2 t2',
+      value v1 ->
+      t2 => t2' ->
+      tm_plus v1 t2 => tm_plus v1 t2'
+
+  where " t '=>' t' " := (step t t').
+
+Lemma value_not_same_as_normal_form:
+   exists t, value t /\ ~ normal_form step t.
+Proof.
+intros.
+unfold normal_form.
+exists (tm_plus (tm_plus (tm_const 1) (tm_const 2)) (tm_const 2)).
+split.
+ apply v_funny.
+ 
+ unfold not.
+ intros.
+ apply H.
+ exists (tm_plus (tm_const (1 + 2)) (tm_const 2)).
+ apply ST_Plus1.
+ apply ST_PlusConstConst.
+Qed.
+
+End Temp1.
+
+Module Temp2.
+
+Inductive value : tm -> Prop :=
+   | v_const : forall n, value (tm_const n).
+
+(*Reserved Notation " t '===>' t' " (at level 40).*)
+
+Inductive step : tm -> tm -> Prop :=
+  | ST_Funny : forall n, (* <---- *)
+      tm_const n ===> tm_plus (tm_const n) (tm_const 0)
+  | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2) ===> tm_const (plus n1 n2)
+  | ST_Plus1 : forall t1 t1' t2,
+      t1 ===> t1' ->
+      tm_plus t1 t2 ===> tm_plus t1' t2
+  | ST_Plus2 : forall v1 t2 t2',
+      value v1 ->
+      t2 ===> t2' ->
+      tm_plus v1 t2 ===> tm_plus v1 t2'
+
+  where " t '===>' t' " := (step t t').
+
+Lemma value_not_same_as_normal_form :
+  exists t, value t /\ ~ normal_form step t.
+Proof.
+exists (tm_const 0).
+split.
+ apply v_const.
+ 
+ unfold normal_form.
+ unfold not.
+ intro H.
+ apply H.
+ exists (tm_plus (tm_const 0) (tm_const 0)).
+ apply ST_Funny.
+Qed.
+
+End Temp2.
+
+Module Temp3.
+
+Inductive value : tm -> Prop :=
+  | v_const : forall n, value (tm_const n).
+
+(*Reserved Notation " t '===>' t' " (at level 40).*)
+
+Inductive step : tm -> tm -> Prop :=
+  | ST_PlusConstConst : forall n1 n2,
+      tm_plus (tm_const n1) (tm_const n2) ===> tm_const (plus n1 n2)
+  | ST_Plus1 : forall t1 t1' t2,
+      t1 ===> t1' ->
+      tm_plus t1 t2 ===> tm_plus t1' t2
+
+  where " t '===>' t' " := (step t t').
+
+Lemma value_not_same_as_normal_form:
+   exists t, ~ value t /\ normal_form step t.
+Proof.
+exists (tm_plus (tm_const 1) (tm_plus (tm_const 0) (tm_const 0))).
+split.
+ intros H.
+ inversion H.
+ 
+ unfold normal_form.
+ intros H.
+ inversion H.
+ inversion H0.
+ inversion H4.
+Qed.
+
+End Temp3.
+
+Module Temp4.
+Inductive tm : Type :=
+   | tm_true : tm
+   | tm_false : tm
+   | tm_if : tm -> tm -> tm -> tm.
+
+Inductive value : tm -> Prop :=
+   | v_true : value tm_true
+   | v_false : value tm_false.
+
+Inductive step : tm -> tm -> Prop :=
+   | ST_IfTrue : forall t1 t2,
+      tm_if tm_true t1 t2 ===> t1
+   | ST_IfFalse : forall t1 t2,
+      tm_if tm_false t1 t2 ===> t2
+   | ST_If : forall t1 t1' t2 t3,
+      t1 ===> t1' ->
+         tm_if t1 t2 t3 ===> tm_if t1' t2 t3
+
+   where " t '===>' t' " := (step t t').
+
+Example bool_step_prop3 :
+     tm_if
+       (tm_if tm_true tm_true tm_true)
+       (tm_if tm_true tm_true tm_true)
+       tm_false
+   ===>
+     tm_if
+       tm_true
+       (tm_if tm_true tm_true tm_true)
+       tm_false.
+Proof.
+apply ST_If.
+apply ST_IfTrue.
+Qed.
+
+Theorem strong_progress: forall t,
+        value t \/ (exists t', t ===> t').
+Proof.
+induction t.
+ left.
+ constructor.
+ 
+ left.
+ constructor.
+ 
+ right.
+ inversion IHt1.
+  inversion H.
+   exists t2.
+   apply ST_IfTrue.
+   
+   exists t3.
+   apply ST_IfFalse.
+   
+  inversion H.
+  exists (tm_if x t2 t3).
+  apply ST_If.
+  assumption.
+Qed.
+
+Theorem step_deterministic :
+  partial_function step.
+Proof.
+unfold partial_function.
+intros x y1 y2 Hy1 Hy2.
+generalize dependent y2.
+induction Hy1.
+ intros.
+ inversion Hy2.
+  reflexivity.
+  
+  subst.
+  inversion H3.
+  
+ intros.
+ inversion Hy2.
+  reflexivity.
+  
+  inversion H3.
+  
+ intros.
+ inversion Hy2.
+  subst.
+  inversion Hy1.
+  
+  subst.
+  inversion Hy1.
+  
+  subst.
+  apply IHHy1 in H3.
+  subst.
+  reflexivity.
+Qed.
+
+Module Temp5.
+
+
+Inductive step : tm -> tm -> Prop :=
+   | ST_IfTrue : forall t1 t2,
+      tm_if tm_true t1 t2 ===> t1
+   | ST_IfFalse : forall t1 t2,
+      tm_if tm_false t1 t2 ===> t2
+   | ST_If : forall t1 t1' t2 t3,
+      t1 ===> t1' ->
+         tm_if t1 t2 t3 ===> tm_if t1' t2 t3
+   | ST_ShortCut : forall v t,
+      value v ->
+         tm_if t v v ===> v
+
+   where " t '===>' t' " := (step t t').
+
+Definition bool_step_prop4 :=
+         tm_if
+            (tm_if tm_true tm_true tm_true)
+            tm_false
+            tm_false
+     ===>
+         tm_false.
+
+Example bool_step_prop4_holds : 
+  bool_step_prop4.
+Proof.
+   unfold bool_step_prop4.
+   apply ST_ShortCut.
+   constructor.
+Qed.
+
+Theorem strong_progress: forall t,
+        value t \/ (exists t', t ===> t').
+Proof.
+   induction t.
+ left.
+ constructor.
+ 
+ left.
+ constructor.
+ 
+ inversion IHt1.
+  right.
+  inversion H.
+   exists t2.
+   constructor.
+   
+   exists t3.
+   constructor.
+   
+  right.
+  inversion H.
+  exists (tm_if x t2 t3).
+  apply ST_If.
+  assumption.
+Qed.
+
+End Temp5.
+End Temp4.
+
+Definition stepmany := refl_step_closure step.
+
+Notation " t '===>*' t' " := (stepmany t t') (at level 40).
+
+Lemma test_stepmany_1:
+   tm_plus
+      (tm_plus (tm_const 0) (tm_const 3))
+      (tm_plus (tm_const 2) (tm_const 4))
+      ===>*
+         tm_const (plus (plus 0 3) (plus 2 4)).
+Proof.
+   eapply rsc_step. apply ST_Plus1. apply ST_PlusConstConst.
+  eapply rsc_step. apply ST_Plus2. apply v_const.
+  apply ST_PlusConstConst.
+  eapply rsc_step. apply ST_PlusConstConst.
+  apply rsc_refl. Qed.
+
+Lemma test_stepmany_2:
+   tm_const 3 ===>* tm_const 3.
+Proof.
+   eapply rsc_refl.
+Qed.
+
+Lemma test_stepmany_3:
+   tm_plus (tm_const 0) (tm_const 3)
+      ===>*
+   tm_plus (tm_const 0) (tm_const 3).
+Proof.
+   eapply rsc_refl.
+Qed.
+
+Lemma test_stepmany_4:
+   tm_plus
+      (tm_const 0)
+      (tm_plus
+         (tm_const 2)
+         (tm_plus (tm_const 0) (tm_const 3)))
+   ===>*
+      tm_plus
+         (tm_const 0)
+         (tm_const (plus 2 (plus 0 3))).
+Proof.
+eapply rsc_step.
+ apply ST_Plus2.
+  apply v_const.
+  
+  apply ST_Plus2.
+   apply v_const.
+   
+   apply ST_PlusConstConst.
+   
+ eapply rsc_step.
+  apply ST_Plus2.
+   apply v_const.
+   
+   apply ST_PlusConstConst.
+   
+  eapply rsc_refl.
+Qed.
+
+Definition step_normal_form := normal_form step.
+
+Definition normal_form_of (t t' : tm) :=
+  (t ===>* t' /\ step_normal_form t').
+
+   (*
+Theorem normal_forms_unique:
+   partial_function normal_form_of.
+Proof.
+   unfold partial_function. unfold normal_form_of. intros x y1 y2 P1 P2.
+   destruct P1 as [P11 P12]. destruct P2 as [P21 P22].
+   generalize dependent y2.
+
+   unfold step_normal_form in P12.
+   unfold step_normal_form.
+   unfold normal_form.
+   unfold normal_form in P12.
+   induction x.
+   intros.
+   unfold stepmany.
+   inversion P11.
+   subst.
+   inversion P21.
+   subst.
+   reflexivity.
+
+   subst.
+   inversion P21.
+   reflexivity.
+
+   subst.
+   inversion H1.
+
+   inversion H.
+   *)
+
+Definition normalizing {X:Type} (R:relation X) :=
+     forall t, exists t',
+         (refl_step_closure R) t t' /\ normal_form R t'.
+
+Lemma stepmany_congr_1 : forall t1 t1' t2,
+      t1 ===>* t1' ->
+         tm_plus t1 t2 ===>* tm_plus t1' t2.
+Proof.
+intros t1 t1' t2 H.
+rsc_cases (induction H) Case.
+ apply rsc_refl.
+  
+  apply rsc_step with (tm_plus y t2).
+    apply ST_Plus1.
+      apply H.
+        
+        apply IHrefl_step_closure.
+Qed.
+
+Lemma stepmany_congr2 : forall t1 t2 t2',
+      value t1 ->
+         t2 ===>* t2' ->
+            tm_plus t1 t2 ===>* tm_plus t1 t2'.
+Proof.
+intros t1 t2 t2'.
+intros H1.
+intros H2.
+induction H2.
+ apply rsc_refl.
+  
+  apply rsc_step with (tm_plus t1 y).
+    apply ST_Plus2.
+       assumption.
+          
+          assumption.
+             
+            assumption.
+Qed.
+
+Theorem step_normalizing :
+  normalizing step.
+Proof.
+  unfold normalizing.
+  tm_cases (induction t) Case.
+    Case "tm_const".
+      exists (tm_const n).
+      split.
+      SCase "l". apply rsc_refl.
+      SCase "r".
+        (* We can use rewrite with "iff" statements, not
+           just equalities: *)
+        rewrite nf_same_as_value. apply v_const.
+    Case "tm_plus".
+      destruct IHt1 as [t1' H1]. destruct IHt2 as [t2' H2].
+      destruct H1 as [H11 H12]. destruct H2 as [H21 H22].
+      rewrite nf_same_as_value in H12. rewrite nf_same_as_value in H22.
+      inversion H12 as [n1]. inversion H22 as [n2].
+      rewrite <- H in H11.
+      rewrite <- H0 in H21.
+      exists (tm_const (plus n1 n2)).
+      split.
+        SCase "l".
+          apply rsc_trans with (tm_plus (tm_const n1) t2).
+          apply stepmany_congr_1. apply H11.
+          apply rsc_trans with 
+             (tm_plus (tm_const n1) (tm_const n2)).
+          apply stepmany_congr2. apply v_const. apply H21.
+          apply rsc_R. apply ST_PlusConstConst.
+        SCase "r".
+          rewrite nf_same_as_value. apply v_const. Qed.
+          
+ Lemma eval__value : forall t1 t2,
+      eval t1 t2 ->
+      value t2.
+ Proof.
+   intros t1 t2 HE.
+   eval_cases (inversion HE) Case; apply v_const. Qed.
+   
+
+   (*
+Theorem eval__stepmany: forall t v,
+  eval t v -> t ===>* v.
+Proof.   
+*)

samples/Coq/Sorting.v

@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Export Sorted.
+Require Export Mergesort.

samples/Coq/Stlc.v

@@ -0,0 +1,733 @@
+
+Require Export SfLib.
+
+Module STLC.
+
+Inductive ty : Type :=
+   | ty_Bool : ty
+   | ty_arrow : ty -> ty -> ty.
+
+Inductive tm : Type :=
+   | tm_var : id -> tm
+   | tm_app : tm -> tm -> tm
+   | tm_abs : id -> ty -> tm -> tm
+   | tm_true : tm
+   | tm_false : tm
+   | tm_if : tm -> tm -> tm -> tm.
+
+Tactic Notation "tm_cases" tactic(first) ident(c) :=
+  first;
+  [ Case_aux c "tm_var" | Case_aux c "tm_app" 
+  | Case_aux c "tm_abs" | Case_aux c "tm_true" 
+  | Case_aux c "tm_false" | Case_aux c "tm_if" ].
+  
+Notation a := (Id 0).
+Notation b := (Id 1).
+Notation c := (Id 2).
+
+Notation idB :=
+   (tm_abs a ty_Bool (tm_var a)).
+   
+Notation idBB :=
+   (tm_abs a (ty_arrow ty_Bool ty_Bool) (tm_var a)).
+   
+Notation idBBBB :=
+   (tm_abs a (ty_arrow (ty_arrow ty_Bool ty_Bool) 
+                         (ty_arrow ty_Bool ty_Bool)) 
+       (tm_var a)).
+       
+Notation k := (tm_abs a ty_Bool (tm_abs b ty_Bool (tm_var a))).
+
+Inductive value : tm -> Prop :=
+  | v_abs : forall x T t,
+      value (tm_abs x T t)
+  | t_true : 
+      value tm_true
+  | t_false : 
+      value tm_false.
+
+Hint Constructors value.
+
+Fixpoint subst (s:tm) (x:id) (t:tm) : tm :=
+   match t with
+   | tm_var x' => if beq_id x x' then s else t
+   | tm_abs x' T t1 => tm_abs x' T (if beq_id x x' then t1 else (subst s x t1))
+   | tm_app t1 t2 => tm_app (subst s x t1) (subst s x t2)
+   | tm_true => tm_true
+   | tm_false => tm_false
+   | tm_if t1 t2 t3 => tm_if (subst s x t1) (subst s x t2) (subst s x t3)
+end.
+
+Reserved Notation "t1 '==>' t2" (at level 40).
+
+Inductive step : tm -> tm -> Prop :=
+ | ST_AppAbs : forall x T t12 v2,
+        value v2 ->
+        (tm_app (tm_abs x T t12) v2) ==> (subst v2 x t12)
+ | ST_App1 : forall t1 t1' t2,
+        t1 ==> t1' ->
+        tm_app t1 t2 ==> tm_app t1' t2
+ | ST_App2 : forall v1 t2 t2',
+        value v1 ->
+        t2 ==> t2' ->
+        tm_app v1 t2 ==> tm_app v1 t2'
+ | ST_IfTrue : forall t1 t2,
+     (tm_if tm_true t1 t2) ==> t1
+ | ST_IfFalse : forall t1 t2,
+     (tm_if tm_false t1 t2) ==> t2
+ | ST_If : forall t1 t1' t2 t3,
+     t1 ==> t1' ->
+     (tm_if t1 t2 t3) ==> (tm_if t1' t2 t3)
+
+where "t1 '==>' t2" := (step t1 t2).
+
+Tactic Notation "step_cases" tactic(first) ident(c) :=
+ first;
+ [ Case_aux c "ST_AppAbs" | Case_aux c "ST_App1" 
+ | Case_aux c "ST_App2" | Case_aux c "ST_IfTrue" 
+ | Case_aux c "ST_IfFalse" | Case_aux c "ST_If" ].
+
+Notation stepmany := (refl_step_closure step).
+Notation "t1 '==>*' t2" := (stepmany t1 t2) (at level 40).
+
+Hint Constructors step.
+
+Lemma step_example3 :
+       (tm_app (tm_app idBBBB idBB) idB)
+  ==>* idB.
+Proof.
+ eapply rsc_step.
+ apply ST_App1.
+ apply ST_AppAbs.
+ apply v_abs.
+ 
+ simpl.
+ eapply rsc_step.
+  apply ST_AppAbs.
+  apply v_abs.
+  
+  simpl.
+  apply rsc_refl.
+Qed.
+
+Definition context := partial_map ty.
+Module Context.
+
+Definition partial_map (A:Type) := id -> option A.
+Definition empty {A:Type} : partial_map A := (fun _ => None).
+Definition extend {A:Type} (Gamma : partial_map A) (x:id) (T : A) :=
+   fun x' => if beq_id x x' then Some T else Gamma x'.
+   
+Lemma extend_eq : forall A (ctxt: partial_map A) x T,
+   (extend ctxt x T) x = Some T.
+Proof.
+   intros. unfold extend. rewrite <- beq_id_refl. auto.
+Qed.
+
+Lemma extend_neq : forall A (ctxt: partial_map A) x1 T x2,
+   beq_id x2 x1 = false ->
+      (extend ctxt x2 T) x1 = ctxt x1.
+Proof.
+intros. unfold extend. rewrite H. auto.
+Qed.
+
+End Context.
+
+Inductive has_type : context -> tm -> ty -> Prop :=
+   | T_Var : forall Gamma x T,
+      Gamma x = Some T ->
+         has_type Gamma (tm_var x) T
+   | T_Abs : forall Gamma x T11 T12 t12,
+      has_type (extend Gamma x T11) t12 T12 ->
+         has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12)
+   | T_App : forall T11 T12 Gamma t1 t2,
+      has_type Gamma t1 (ty_arrow T11 T12) ->
+         has_type Gamma t2 T11 ->
+            has_type Gamma (tm_app t1 t2) T12
+   | T_True : forall Gamma,
+      has_type Gamma tm_true ty_Bool
+   | T_False : forall Gamma,
+      has_type Gamma tm_false ty_Bool
+   | T_If : forall t1 t2 t3 T Gamma,
+      has_type Gamma t1 ty_Bool ->
+      has_type Gamma t2 T ->
+      has_type Gamma t3 T ->
+      has_type Gamma (tm_if t1 t2 t3) T.
+      
+Tactic Notation "has_type_cases" tactic(first) ident(c) :=
+  first;
+  [ Case_aux c "T_Var" | Case_aux c "T_Abs" 
+  | Case_aux c "T_App" | Case_aux c "T_True" 
+  | Case_aux c "T_False" | Case_aux c "T_If" ].
+
+Hint Constructors has_type.
+
+Hint Unfold beq_id beq_nat extend.
+
+Example typing_example_2_full :
+  has_type empty
+    (tm_abs a ty_Bool
+       (tm_abs b (ty_arrow ty_Bool ty_Bool)
+          (tm_app (tm_var b) (tm_app (tm_var b) (tm_var a)))))
+    (ty_arrow ty_Bool (ty_arrow (ty_arrow ty_Bool ty_Bool) ty_Bool)).
+Proof.
+apply T_Abs.
+apply T_Abs.
+apply T_App with (T11 := ty_Bool).
+ apply T_Var.
+ unfold extend.
+ simpl.
+ reflexivity.
+ 
+ apply T_App with (T11 := ty_Bool).
+  apply T_Var.
+  unfold extend.
+  simpl.
+  reflexivity.
+  
+  apply T_Var.
+  unfold extend.
+  simpl.
+  reflexivity.
+Qed.
+
+Example typing_example_3 :
+  exists T, 
+    has_type empty
+      (tm_abs a (ty_arrow ty_Bool ty_Bool)
+         (tm_abs b (ty_arrow ty_Bool ty_Bool)
+            (tm_abs c ty_Bool
+               (tm_app (tm_var b) (tm_app (tm_var a) (tm_var c))))))
+      T.
+
+Proof with auto.
+exists
+ (ty_arrow (ty_arrow ty_Bool ty_Bool)
+    (ty_arrow (ty_arrow ty_Bool ty_Bool) (ty_arrow ty_Bool ty_Bool))).
+apply T_Abs.
+apply T_Abs.
+apply T_Abs.
+apply T_App with (T11 := ty_Bool).
+ apply T_Var.
+ unfold extend.
+ simpl.
+ reflexivity.
+ 
+ apply T_App with (T11 := ty_Bool).
+  auto.
+  
+  auto.
+Qed.
+
+
+Theorem coiso : forall a b e,
+   a ==>* b ->
+      tm_app a e ==>* tm_app b e.
+Proof.
+intros.
+induction H.
+ apply rsc_refl.
+ 
+ apply rsc_step with (tm_app y e).
+  apply ST_App1.
+  assumption.
+  
+  assumption.
+Qed.
+
+Theorem reptrans : forall a b c,
+   a ==>* b ->
+      b ==>* c ->
+         a ==>* c.
+Proof.
+
+intros a b c H.
+induction H.
+ intros.
+ assumption.
+ 
+ intros H1.
+ apply IHrefl_step_closure in H1.
+ apply rsc_step with y.
+  assumption.
+  
+  assumption.
+Qed.
+
+(* TODO
+Example typing_nonexample_3 :
+  ~ (exists S, exists T,
+        has_type empty 
+          (tm_abs a S
+             (tm_app (tm_var a) (tm_var a)))
+          T).
+Proof.
+*)
+
+Inductive appears_free_in : id -> tm -> Prop :=
+  | afi_var : forall x,
+      appears_free_in x (tm_var x)
+  | afi_app1 : forall x t1 t2,
+      appears_free_in x t1 -> appears_free_in x (tm_app t1 t2)
+  | afi_app2 : forall x t1 t2,
+      appears_free_in x t2 -> appears_free_in x (tm_app t1 t2)
+  | afi_abs : forall x y T11 t12,
+      y <> x ->
+      appears_free_in x t12 ->
+      appears_free_in x (tm_abs y T11 t12)
+  | afi_if1 : forall x t1 t2 t3,
+      appears_free_in x t1 ->
+      appears_free_in x (tm_if t1 t2 t3)
+  | afi_if2 : forall x t1 t2 t3,
+      appears_free_in x t2 ->
+      appears_free_in x (tm_if t1 t2 t3)
+  | afi_if3 : forall x t1 t2 t3,
+      appears_free_in x t3 ->
+      appears_free_in x (tm_if t1 t2 t3).
+      
+Tactic Notation "afi_cases" tactic(first) ident(c) :=
+  first;
+  [ Case_aux c "afi_var"
+  | Case_aux c "afi_app1" | Case_aux c "afi_app2" 
+  | Case_aux c "afi_abs" 
+  | Case_aux c "afi_if1" | Case_aux c "afi_if2" 
+  | Case_aux c "afi_if3" ].
+
+Hint Constructors appears_free_in.
+
+Definition closed (t:tm) :=
+  forall x, ~ appears_free_in x t.
+  
+Lemma free_in_context : forall x t T Gamma,
+  appears_free_in x t ->
+  has_type Gamma t T ->
+  exists T', Gamma x = Some T'.
+Proof.
+  intros. generalize dependent Gamma. generalize dependent T.
+  afi_cases (induction H) Case; 
+         intros; try solve [inversion H0; eauto].
+  Case "afi_abs".
+    inversion H1; subst.
+    apply IHappears_free_in in H7.
+    apply not_eq_beq_id_false in H.
+    rewrite extend_neq in H7; assumption.
+Qed.
+
+Corollary typable_empty__closed : forall t T, 
+    has_type empty t T ->
+    closed t.
+Proof.
+intros t T H x H1.
+remember (@empty ty) as Gamma.
+assert (exists t' : _, Gamma x = Some t').
+ apply free_in_context with (t := t) (T := T).
+  assumption.
+  
+  assumption.
+  
+ inversion H0.
+ rewrite HeqGamma in H2.
+ inversion H2.
+Qed.
+
+Lemma context_invariance : forall Gamma Gamma' t S,
+     has_type Gamma t S ->
+     (forall x, appears_free_in x t -> Gamma x = Gamma' x) ->
+     has_type Gamma' t S.
+Proof with auto.
+intros.
+generalize dependent Gamma'.
+has_type_cases (induction H) Case; intros; auto.
+ apply T_Var.
+ rewrite <- H0...
+ 
+ apply T_Abs.
+ apply IHhas_type.
+ intros x0 Hafi.
+ unfold extend.
+ remember (beq_id x x0) as e.
+ destruct e.
+  reflexivity.
+  
+  auto.
+  apply H0.
+  apply afi_abs.
+   auto.
+   eauto   .
+   apply beq_id_false_not_eq.
+   rewrite Heqe.
+   reflexivity.
+   
+   assumption.
+   
+ apply T_App with T11.
+  auto.
+  
+  auto.
+Qed.
+
+Lemma substitution_preserves_typing : forall Gamma x U v t T,
+   has_type (extend Gamma x U) t T ->
+      has_type empty v U ->
+         has_type Gamma (subst v x t) T.
+Proof with eauto.
+   intros Gamma x U v t T Ht Hv.
+   generalize dependent Gamma.
+   generalize dependent T.
+   tm_cases (induction t) Case; intros T Gamma H; inversion H; subst; simpl...
+   Case "tm_var".
+       rename i into y. remember (beq_id x y) as e. destruct e.
+       SCase "x=y".
+         apply beq_id_eq in Heqe. subst.
+         rewrite extend_eq in H2.
+         inversion H2; subst.
+         clear H2.
+           eapply context_invariance...
+           intros x Hcontra.
+           destruct (free_in_context _ _ T empty Hcontra) as (T', HT')...
+           inversion HT'.
+
+           apply T_Var.
+           rewrite extend_neq in H2.
+            assumption.
+
+            rewrite Heqe.
+            reflexivity.
+
+          rename i into y.
+          apply T_Abs.
+          remember (beq_id x y) as e.
+          destruct e.
+           eapply context_invariance...
+           apply beq_id_eq in Heqe.
+           subst.
+           intros x Hafi.
+           unfold extend.
+           destruct (beq_id y x).
+            reflexivity.
+
+            reflexivity.
+
+           apply IHt.
+           eapply context_invariance...
+           intros x0 Hafi.
+           unfold extend.
+           remember (beq_id y x0) as Coiso1.
+           remember (beq_id x x0) as Coiso2.
+           destruct Coiso1.
+            auto.
+            eauto   .
+            destruct Coiso2.
+             eauto   .
+             auto.
+             apply beq_id_eq in HeqCoiso1.
+             apply beq_id_eq in HeqCoiso2.
+             subst.
+             assert (x0 <> x0).
+              apply beq_id_false_not_eq.
+              rewrite Heqe.
+              auto.
+
+              apply ex_falso_quodlibet.
+              apply H0.
+              reflexivity.
+
+             reflexivity.
+
+            destruct Coiso2.
+             auto.
+
+             auto.
+Qed.
+
+Theorem preservation : forall t t' T,
+     has_type empty t T ->
+     t ==> t' ->
+     has_type empty t' T.
+Proof.
+remember (@empty ty) as Gamma.
+intros t t' T HT.
+generalize dependent t'.
+induction HT.
+ intros t' H1.
+ inversion H1.
+ 
+ intros t' H1.
+ inversion H1.
+ 
+ intros t' H1.
+ inversion H1.
+  apply substitution_preserves_typing with T11.
+   subst.
+   inversion HT1.
+   subst.
+   apply H2.
+   
+   subst.
+   assumption.
+   
+  subst.
+  apply T_App with T11.
+   apply IHHT1.
+    reflexivity.
+    
+    assumption.
+    
+   assumption.
+   
+  subst.
+  apply T_App with T11.
+   assumption.
+   
+   apply IHHT2.
+    reflexivity.
+    
+    assumption.
+    
+ intros t' H.
+ inversion H.
+ 
+ intros t' H.
+ inversion H.
+ 
+ intros t' H.
+ inversion H.
+  subst.
+  assumption.
+  
+  subst.
+  assumption.
+  
+  subst.
+  apply T_If.
+   apply IHHT1.
+    reflexivity.
+    
+    assumption.
+    
+   assumption.
+   
+   assumption.
+Qed.
+
+Theorem progress : forall t T,
+     has_type empty t T ->
+     value t \/ exists t', t ==> t'.
+Proof.
+intros t T.
+intros H.
+remember (@empty ty) as Gamma.
+induction H.
+ rewrite HeqGamma in H.
+ unfold empty in H.
+ inversion H.
+ 
+ left.
+ apply v_abs.
+ 
+ right.
+ assert (value t1 \/ (exists t' : tm, t1 ==> t')).
+  apply IHhas_type1.
+  assumption.
+  
+  assert (value t2 \/ (exists t' : tm, t2 ==> t')).
+   apply IHhas_type2.
+   assumption.
+   
+   inversion H1.
+    inversion H2.
+     inversion H3.
+      subst.
+      exists (subst t2 x t).
+      apply ST_AppAbs.
+      assumption.
+      
+      subst.
+      inversion H.
+      
+      subst.
+      inversion H.
+      
+     inversion H4.
+     exists (tm_app t1 x).
+     apply ST_App2.
+      assumption.
+      
+      assumption.
+      
+    inversion H3.
+    exists (tm_app x t2).
+    apply ST_App1.
+    assumption.
+    
+ left.
+ auto.
+ 
+ left.
+ auto.
+ 
+ right.
+ assert (value t1 \/ (exists t' : tm, t1 ==> t')).
+  apply IHhas_type1.
+  assumption.
+  
+  inversion H2.
+   inversion H3.
+    subst.
+    inversion H.
+    
+    subst.
+    exists t2.
+    apply ST_IfTrue.
+    
+    subst.
+    exists t3.
+    apply ST_IfFalse.
+    
+   inversion H3.
+   exists (tm_if x t2 t3).
+   apply ST_If.
+   assumption.
+Qed.
+
+Theorem progress' : forall t T,
+     has_type empty t T ->
+     value t \/ exists t', t ==> t'.
+Proof.
+intros t.
+tm_cases (induction t) Case; intros T Ht; auto.
+ inversion Ht.
+ inversion H1.
+ 
+ right.
+ inversion Ht.
+ subst.
+ assert (value t1 \/ (exists t' : tm, t1 ==> t')).
+  apply IHt1 with (T := ty_arrow T11 T).
+  assumption.
+  
+  assert (value t2 \/ (exists t' : tm, t2 ==> t')).
+   apply IHt2 with T11.
+   assumption.
+   
+   inversion H.
+    inversion H1.
+     subst.
+     inversion H0.
+      exists (subst t2 x t).
+      apply ST_AppAbs.
+      assumption.
+      
+      inversion H3.
+      exists (tm_app (tm_abs x T0 t) x0).
+      apply ST_App2.
+       assumption.
+       
+       assumption.
+       
+     subst.
+     inversion H2.
+     
+     subst.
+     inversion H2.
+     
+    inversion H1.
+    exists (tm_app x t2).
+    apply ST_App1.
+    assumption.
+    
+ right.
+ inversion Ht.
+ subst.
+ assert (value t1 \/ (exists t' : tm, t1 ==> t')).
+  apply IHt1 with ty_Bool.
+  assumption.
+  
+  assert (value t2 \/ (exists t' : tm, t2 ==> t')).
+   apply IHt2 with T.
+   assumption.
+   
+   assert (value t3 \/ (exists t' : tm, t3 ==> t')).
+    apply IHt3 with T.
+    assumption.
+    
+    inversion H.
+     inversion H2.
+      subst.
+      inversion H3.
+      
+      subst.
+      subst.
+      exists t2.
+      apply ST_IfTrue.
+      
+      exists t3.
+      apply ST_IfFalse.
+      
+     inversion H2.
+     exists (tm_if x t2 t3).
+     apply ST_If.
+     assumption.
+Qed.
+
+Theorem types_unique : forall t T Gamma,
+   has_type Gamma t T ->
+      (forall T', has_type Gamma t T' -> T' = T).
+Proof.
+intros t T Gamma H.
+induction H.
+ intros T'.
+ intros H1.
+ inversion H1.
+ subst.
+ subst.
+ auto.
+ eauto   .
+ inversion H1.
+ subst.
+ assert (Some T = Some T').
+  rewrite <- H3.
+  rewrite <- H.
+  reflexivity.
+  
+  inversion H0.
+  reflexivity.
+  
+ intros T'.
+ intros H1.
+ inversion H1.
+ subst.
+ assert (T1 = T12).
+  apply IHhas_type.
+  assumption.
+  
+  rewrite H0.
+  reflexivity.
+  
+ intros T' H1.
+ subst.
+ inversion H1.
+ subst.
+ assert (ty_arrow T0 T' = ty_arrow T11 T12).
+  apply IHhas_type1.
+  assumption.
+  
+  inversion H2.
+  reflexivity.
+  
+ intros T'.
+ intros H.
+ inversion H.
+ reflexivity.
+ 
+ intros.
+ inversion H.
+ reflexivity.
+ 
+ intros T'.
+ intros H2.
+ inversion H2.
+ subst.
+ apply IHhas_type2.
+ assumption.
+Qed.