Title: Theory / Unimportant / CS / Programming / Coq / Software foundation
Tags: hasNotNewEffectReturnsMeaning FromInstruction algoToProg computer_to_instruction type some_instruction
On every note of this deck, unless a note says otherwise:
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html

Name: Functional programing
Definition: If a procedure or method has no side effects, then (ignoring efficiency) all we need to understand about it is how it maps inputs to outputs
Page: softwarefoundations
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Definition2: emphasizes the use of functions (or methods) as first-class values

Name: A first class value
Definition: A value which can be passed as arguments to other functions
Page: softwarefoundations
Chapter: FUNCTIONAL PROGRAMMING IN COQ

Typ: bool
Meaning: A type with two constructor, true and false
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: type

Typ: foo ->bar
Meaning: The type of functions sending foo to bar
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: type

Instruction: Module foo
  bar
end foo.
Effect: Create a module named foo whose content is bar
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: (foo_1 ... foo_n: buz)
Effect: State that all parameters foo_i have type buz
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Name: A tactic
Definition: A command that is used between Proof and Qed to guide the process of checking some claim we are making.
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Example: intros foo
Example2: reflexivity

Effect: Start a proof of a new subgoal
Language: coq
Context: Proof
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog
Name: -
+
*

Instruction: {foo}
Effect: foo is a proof of a subgoal
Language: coq
Context: Proof
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Name: A goal
Definition: Something which should currently be proven
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Context: Proof, coq

Name: A subgoal of G
Definition: A goal of a statement introduced during the proof of G
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: G a goal
Context: Proof

Name: intros [bar_1,1 ... bar_1,n_1|...|bar_m,1 ... bar_m,n_m]
Definition: Similar to:
intros foo.
destruct foo as [bar_1,1 ... bar_1,n_1|...|bar_m,1 ... bar_m,n_m]
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Context: Proof

Name: A precedence level
Definition: A number, associated to symbol, which indicates how to parenthesis a compound expression with multiple symbols.
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Context: Proof
Typ: Int between 0 and 100

Question: In a compound expression with multiple symbols, the symbol first evaluated is
Answer: the one with the least precedence level
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Chapter: FUNCTIONAL PROGRAMMING IN COQ

Name: The associativity of *
Definition: A rule which state which * must be evaluated first.
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: * a symbol

Instruction: (at level n)
Effect: State that * 's precedence level is n
Language: coq
Context: Notation
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: * a symbol
Extra: prog

Instruction: (foo associativity)
Effect: State that * 's associativity is foo
Language: coq
Context: Notation
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: * a symbol
Extra: prog
Assuming: foo is left, right or no

Instruction: :foo
Effect: The current notation is limited to the scope named foo
Language: coq
Context: Notation
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: * a symbol
Extra: prog

Instruction: foo%s
Effect: foo interpreted as a value in scope s
Language: coq
Context: Notation
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: foo a symbol
s a scope
Extra: prog

Typ: Inductive foo: Type :=
  | bar_1:buz_1
  ...
  | bar_n:buz_n
Meaning: Define a type foo with exactly the n distinct constructor enumerated
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Assuming: each buz_i is a type either foo or foo'=>foo

Name: A constructor expression
Definition: A constructor, applied to as many parameter as in its definition, correctly typed
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Context: coq

Name: Tuple
Definition: A type with a single constructor
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Context: coq