Skip to content
Snippets Groups Projects
Select Git revision
  • d4668235b92259fa5ec26f33f3bf81f4c5f86a27
  • master default protected
  • home-exam
  • dsi_debug
  • rtt_timing
  • timing_task
  • timing_resources
  • main.rs
  • rtic6
  • v1.0
10 results

STM32F401.svd

Blame
  • Forked from Per Lindgren / rtic_f4xx_nucleo
    Source project has a limited visibility.
    peano_nat.mlw 3.22 KiB
    module Nat
    
      type nat = O | S nat
      
      function add (n1 n2 : nat) : nat =
        match n1 with
        | O   -> n2
        | S n -> S (add n n2)
        end 
    
      function (+) (a b : nat) : nat = add a b
      
      use int.Int
      goal g:
        forall x. x = 1 -> x > 0
    end
    
    module TestAdd
    
      use Nat
    
      goal g_0_0: (* 0 + 0 = 0 *)
        O + O = O
      (* solved by "compute_in_goal" *)
    
      goal g_0_1: (* 0 + 1 = 1 *)
        O + S O = S O
      (* solved by "compute_in_goal" *)
    
      goal g_2_1: (* 2 + 1 = 3 *)
        S (S O) + S O = S (S (S O)) 
      (* solved by "compute_in_goal" *)
      
    end
    
    module Inconsistency
    
      lemma introduce: true -> false   (* <-- introduces inconsistency *)
      
      lemma exposed:   true -> false   (* <-- exposed to inconsistency *)
    
      (* 
        incosisitency applies in this scope,
        and all scopes the "use" this module (transitively)
      *)  
    end
    
    
    module Add
    
      use Nat
      
      goal plus_ol: 
        forall n. O + n = n
      (* solved by "compute_in_goal" *)
        
      goal plus_o_right:
        forall n. n + O = n
      (* solved by numerous transformations *)
         
      
      goal plus_o_right_altergo:
        forall n. n + O = n
      (* solved by two simple transofrmations and SMT solver
         "inline_goal"
         "induction_ty_lex"
         "altergo" 
      *)
      
      (* we want to prove commutativity *)